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. © Springer-Verlag Berlin Heidelberg 2001.
Cite
CITATION STYLE
Schmitt, S., Lorigo, L., Kreitz, C., & Nogin, A. (2001). JProver: Integrating connection-based theorem proving into interactive proof assistants. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2083 LNAI, pp. 421–426). Springer Verlag. https://doi.org/10.1007/3-540-45744-5_34
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
