2005 | OriginalPaper | Buchkapitel
Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic
verfasst von : Jens Otten
Erschienen in: Automated Reasoning with Analytic Tableaux and Related Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.