JProver: Integrating connection-based theorem proving into interactive proof assistants. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element