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.
Keywords for this software
References in zbMATH (referenced in 12 articles )
Showing results 1 to 12 of 12.
- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
- Otten, Jens: MleanCoP: a connection prover for first-order modal logic (2014)
- Benzmüller, Christoph; Raths, Thomas: HOL based first-order modal logic provers (2013)
- Otten, Jens: A non-clausal connection calculus (2011)
- Holen, Bjarne; Johnsen, Einar Broch; Waaler, Arild: Proof search for the first-order connection calculus in Maude (2009)
- McLaughlin, Sean; Pfenning, Frank: Efficient intuitionistic theorem proving with the polarized inverse method (2009)
- Otten, Jens: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic. (System descriptions) (2008)
- Sutcliffe, Geoff: The CADE-21 automated theorem proving system competition (2008)
- Antonsen, Roger; Waaler, Arild: A labelled system for IPL with variable splitting (2007)
- Raths, Thomas; Otten, Jens; Kreitz, Christoph: The ILTP problem library for intuitionistic logic (2007)
- Otten, Jens: Clausal connection-based theorem proving in intuitionistic first-order logic (2005)
- Raths, Thomas; Otten, Jens; Kreitz, Christoph: The ILTP library: Benchmarking automated theorem provers for intuitionistic logic (2005)