Clausal connection-based theorem proving in intuitionistic first-order logic. We present a clausal connection calculus for first-order intuitionistic logic. It extends the classical connection calculus by adding prefixes that encode the characteristics of intuitionistic logic. Our calculus is based on a clausal matrix characterisation for intuitionistic logic, which we prove correct and complete. The calculus was implemented by extending the classical prover leanCoP. We present some details of the implementation, called Emphasis ileanCoP, and experimental results.

References in zbMATH (referenced in 16 articles )

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

  1. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  2. Pavlov, V. A.; Pak, V. G.: Theorem prover for intuitionistic logic based on the inverse method (2018)
  3. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  4. Dyckhoff, Roy: Intuitionistic decision procedures since Gentzen (2016)
  5. Otten, Jens: MleanCoP: a connection prover for first-order modal logic (2014)
  6. Benzmüller, Christoph; Raths, Thomas: HOL based first-order modal logic provers (2013)
  7. Benzmüller, Christoph; Otten, Jens; Raths, Thomas: Implementing and evaluating provers for first-order modal logics (2012)
  8. Otten, Jens: A non-clausal connection calculus (2011)
  9. Holen, Bjarne; Johnsen, Einar Broch; Waaler, Arild: Proof search for the first-order connection calculus in Maude (2009)
  10. McLaughlin, Sean; Pfenning, Frank: Efficient intuitionistic theorem proving with the polarized inverse method (2009)
  11. Otten, Jens: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic. (System descriptions) (2008)
  12. Sutcliffe, Geoff: The CADE-21 automated theorem proving system competition (2008)
  13. Antonsen, Roger; Waaler, Arild: A labelled system for IPL with variable splitting (2007)
  14. Raths, Thomas; Otten, Jens; Kreitz, Christoph: The ILTP problem library for intuitionistic logic (2007)
  15. Otten, Jens: Clausal connection-based theorem proving in intuitionistic first-order logic (2005)
  16. Raths, Thomas; Otten, Jens; Kreitz, Christoph: The ILTP library: Benchmarking automated theorem provers for intuitionistic logic (2005)