RE: [Caml-list] Implementation of a prover

["Harrison, John R" <john.r.harrison@intel.com>]

David Baelde writes:

| There are well-known implementation techniques for
| depth-first theorem proving, using continuation-passing
| style (success/failure continuations). But these techniques
| do not easily allow the building of a proof witness. This is
| nice when you have a working proof-search procedure but not
| when you're still playing with a logic, trying to find the
| right procedure or more generally when you just want an
| interactive prover.

I don't know exactly what theorem-proving algorithm you have
in mind, but I guess you mean some "top down" method like free
variable tableaux, Prolog or model elimination.

An approach that I've found effective is to pass along a
closure that will create the proof when applied to a suitable
argument (e.g. the final instantiation of the free variables).
In an algorithm where you explore a large search space but
eventually get a small proof, you postpone any real proof
construction until it's useful, not just an intermediate
result in a failed branch. This is particularly valuable if
your inference process is relatively expensive, as in a
traditional LCF-style prover.

Of course, an alternative is just to pass along some simple
concrete data structure like a tree. Again this fits easily
into the continuation-passing style. But closures can be a
bit more flexible, and OCaml seems to handle closures very
efficiently, so one needn't be afraid to use them.

You can find an example in the code on my Web page, with
a proof-less tableau prover "tableau" here:

  http://www.cl.cam.ac.uk/~jrh13/atp/OCaml/tableaux.ml

and a proof-producing "tableau" function here:

  http://www.cl.cam.ac.uk/~jrh13/atp/OCaml/checking.ml

You can see that they are structurally very close.

John.