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 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
- Otten, Jens: Nanocop: a non-clausal connection prover (2016)
- Otten, Jens: A non-clausal connection calculus (2011)
- 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)
- Goré, Rajeev (ed.); Leitsch, Alexander (ed.); Nipkow, Tobias (ed.): Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings (2001)
- Schmitt, Stephan; Lorigo, Lori; Kreitz, Christoph; Nogin, Aleksey: JProver: Integrating connection-based theorem proving into interactive proof assistants (2001)