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
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Otten, Jens: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic. (System descriptions) (2008)
- Raths, Thomas; Otten, Jens; Kreitz, Christoph: The ILTP problem library for intuitionistic logic (2007)
- Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E.: Innovations in computational type theory using Nuprl (2006)
- Otten, Jens: Clausal connection-based theorem proving in intuitionistic first-order logic (2005)
- Kreitz, Christoph: Building reliable, high-performance networks with the Nuprl proof development system (2004)
- Kreitz, Christoph; Mantel, Heiko: A matrix characterization for multiplicative exponential linear logic (2004)
- Schmitt, Stephan; Lorigo, Lori; Kreitz, Christoph; Nogin, Aleksey: JProver: Integrating connection-based theorem proving into interactive proof assistants (2001)