Sciweavers

Share
TABLEAUX
2005
Springer

Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic

10 years 19 days ago
Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic
Abstract. 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 ileanCoP, and experimental results.
Jens Otten
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TABLEAUX
Authors Jens Otten
Comments (0)
books