An Efficient Refiner for First-order Intuitionistic Logic (Part II)
by Stephan Schmitt
I will present JProver, an efficient refiner for first-order
intuitionistic logic, as well as its integration into NuPRL-5.
JProver consists of two components, a connection-based proof
procedure and a proof reconstruction component, which constructs
sequent proofs from the efficiently generated connection proofs.
A demonstration of JProver will be given for full first-order logic. The prover is called as a tactic from a NuPRL sequent during a proof session. It returns a proof tree in the first-order fragment of ITT, which will be eventually applied to the original NuPRL sequent.
I will illustrate the architecture of the two JProver components as well as the interface to NuPRL-5. Finally, I will discuss the representation of the resulting proof trees within NuPRL-5.