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 8 articles )
Showing results 1 to 8 of 8.
- 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)