1 theory Oracle

     1 theory Oracle

     2 imports "../Appendix"

     2 imports "../Appendix"

     4 begin

     3 begin

     5 

     4 

     6 section {* Writing an Oracle (TBD)\label{rec:oracle} *} 

     5 section {* Writing an Oracle (TBD)\label{rec:oracle} *} 

     7 

     6 

     8 text {*

     7 text {*

    30   Assume, that we have a decision procedure for such formulae, implemented

    29   Assume, that we have a decision procedure for such formulae, implemented

    31   in ML. Since we do not care how it works, we will use it here as an

    30   in ML. Since we do not care how it works, we will use it here as an

    32   ``external solver'':

    31   ``external solver'':

    33 *}

    32 *}

    34 

    33 

    36 

    35 

    37 text {*

    36 text {*

    38   We do, however, know that the solver provides a function

    37   We do, however, know that the solver provides a function

    39   @{ML IffSolver.decide}.

    38   @{ML IffSolver.decide}.

    40   It takes a string representation of a formula and returns either

    39   It takes a string representation of a formula and returns either