# * 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.