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

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.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
• Keywords: Automated Reasoning, CADE 2001, Interactive Proof Assistants, Nuprl Proof Development, Sequent-style Proof Objects