Skip to main content
PRL Project

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.