2005 | OriginalPaper | Chapter
Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic
Author : Jens Otten
Published in: Automated Reasoning with Analytic Tableaux and Related Methods
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.