Implementation of a prover

David Baelde
 Harrison, John R
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20070411 (23:55) 
From:  Harrison, John R <john.r.harrison@i...> 
Subject:  RE: [Camllist] Implementation of a prover 
David Baelde writes:  There are wellknown implementation techniques for  depthfirst theorem proving, using continuationpassing  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 proofsearch 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 theoremproving 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 LCFstyle prover. Of course, an alternative is just to pass along some simple concrete data structure like a tree. Again this fits easily into the continuationpassing 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 proofless tableau prover "tableau" here: http://www.cl.cam.ac.uk/~jrh13/atp/OCaml/tableaux.ml and a proofproducing "tableau" function here: http://www.cl.cam.ac.uk/~jrh13/atp/OCaml/checking.ml You can see that they are structurally very close. John.