Skip to main content
PRL Project

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

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

International Joint Conference on Automated Reasoning, (IJCAR 2001).

  • unofficial copies PDF], [PS]
  • Slides of the conference presentation PS, PDF

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.

bibTex ref: SLKN01

cite link