Implementation of a prover

Implementation of a prover

[David Baelde]

Hi list,

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've started to look for a way to define rules as tactics in such a
way that these core functions can be used with or without a proof
witness construction procedure. I've had enough for today and I wanted
to know if anyone done that or knows a link to anything like that.

Any idea?
-- 
David

RE: [Caml-list] Implementation of a prover

[Harrison, John R]

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.