JProver

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.


References in zbMATH (referenced in 13 articles , 1 standard article )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Färber, Michael; Kaliszyk, Cezary: Certification of nonclausal connection tableaux proofs (2019)
  2. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  3. Pavlov, V. A.; Pak, V. G.: Theorem prover for intuitionistic logic based on the inverse method (2018)
  4. Otten, Jens: Nanocop: a non-clausal connection prover (2016)
  5. Otten, Jens: A non-clausal connection calculus (2011)
  6. Otten, Jens: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic. (System descriptions) (2008)
  7. Raths, Thomas; Otten, Jens; Kreitz, Christoph: The ILTP problem library for intuitionistic logic (2007)
  8. Allen, S. F.; Bickford, M.; Constable, R. L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E.: Innovations in computational type theory using Nuprl (2006)
  9. Otten, Jens: Clausal connection-based theorem proving in intuitionistic first-order logic (2005)
  10. Kreitz, Christoph: Building reliable, high-performance networks with the Nuprl proof development system (2004)
  11. Kreitz, Christoph; Mantel, Heiko: A matrix characterization for multiplicative exponential linear logic (2004)
  12. 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)
  13. Schmitt, Stephan; Lorigo, Lori; Kreitz, Christoph; Nogin, Aleksey: JProver: Integrating connection-based theorem proving into interactive proof assistants (2001)