KnowledgeBase » 
SEMINAR
» ID = 509
An Efficient Refiner for First-order Intuitionistic Logic (Part II)
by Stephan Schmitt
1999-2000
Comment
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.