Jprover: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants.

Stephan Schmitt, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin
Jprover: Integrating connection-based theorem proving into interactive proof assistants.
In International Joint Conference on Automated Reasoning, volume 2083 of Lecture Notes in Artificial Intelligence, pages 421-426. Springer-Verlag, 2001:
PDF (131 KB), PostScript (392KB), LNCS Entry

Slides from the IJCAR'01 presentation: PDF (312KB), Gzipped PostScript (551KB), PostScript (2366KB)

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.

Back to my publications

Last update: Monday, January 26, 2004 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)