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.
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.

		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" }