Skip to main content
PRL Project

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.