An Efficient Refiner for First-order Intuitionistic Logic
by Stephan Schmitt
I will present the architecture of JProver, an efficient refiner
for first-order intuitionistic logic. The refiner will eventually
be connected to the NuPRL-5 architecture.
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 these two components will be given for the propositional fragment, as well as a comparison to tactic based provers for intuitionistic logic.
Finally, I will discuss some aspects concerning of the interface between JProver and NuPRL-5.