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