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

Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Alexey Nogin.

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


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.

Paper is available in
postscript and pdf format
  Slides of the conference presentation are available in compressed postscript and pdf format
(Presentation: Lori Lorigo)

Bibtex Entry

Back to overview of papers
@InProceedings{inp:Schmitt+01a, author = "Stephan Schmitt and Lori Lorigo and Christoph Kreitz and Alexey Nogin", title = "{{\sf JProver}}: Integrating Connection-based Theorem Proving into Interactive Proof Assistants", booktitle = "International Joint Conference on Automated Reasoning", year = "2001", editor = "R. Gore and A. Leitsch and T. Nipkow", volume = "2083", series = "Lecture Notes in Artificial Intelligence", pages = "421--426", publisher = "Springer Verlag" }