JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants

unofficial copies [PDF], [PS]


by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin

International Joint Conference on Automated Reasoning (IJCAR 2001), R. Gore, A. Leitsch, and T. Nipkow (eds.), LNAI 2083, pp. 421-426, Springer-Verlag, 2001.

Abstract

JProver is a first-order intuitionistic theorem prover that creates sequent-style proof objects and can serve as a proof engine in interactive proof assistants with expressive constructive logics. This paper gives a brief overview of JProver's proof technique, the generation of proof objects, and its integration into the Nuprl proof development system.

Slides of the conference presentation are available in compressed [PS] and [PDF] format.