Towards an efficient prover for the C₁ paraconsistent logic

DOI10.1016/J.ENTCS.2009.11.007MaRDI QIDQ5170293zbMATH OpenOpenAlexFDO

Authors Adolfo Neto, Celso A. A. Kaestner, Marcelo Finger

Publication date 23 July 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1202.4144

zbMATH Keywords

paraconsistent logicstableaux systemsKE system\(C_{1}\) logicproblem families

Mathematics Subject Classification ID

Paraconsistent logics (03B53) Mechanization of proofs and logical operations (03B35)

Abstract: The KE inference system is a tableau method developed by Marco Mondadori which was presented as an improvement, in the computational efficiency sense, over Analytic Tableaux. In the literature, there is no description of a theorem prover based on the KE method for the C1 paraconsistent logic. Paraconsistent logics have several applications, such as in robot control and medicine. These applications could benefit from the existence of such a prover. We present a sound and complete KE system for C1, an informal specification of a strategy for the C1 prover as well as problem families that can be used to evaluate provers for C1. The C1 KE system and the strategy described in this paper will be used to implement a KE based prover for C1, which will be useful for those who study and apply paraconsistent logics.

Recommendations

• A reasoning method for a paraconsistent logic
• scientific article; zbMATH DE number 823609
• scientific article; zbMATH DE number 881599
• Some recent applications of paraconsistent systems to AI
• Aspects of Paraconsistent Logic

Cites work

• scientific article; zbMATH DE number 487144 (Why is no real title available?)
• scientific article; zbMATH DE number 551010 (Why is no real title available?)
• scientific article; zbMATH DE number 2196615 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• A reasoning method for a paraconsistent logic
• A semantical analysis of the calculi \(C_n\)
• Analytical tableaux for da Costa's hierarchy of paraconsistent logics \(C_n\), \(1\leq n<\omega\)
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Logics of formal inconsistency
• Tableau methods for classical propositional logic
• The Taming of the Cut. Classical Refutations with Analytic Cut

Cited in

(3)

• Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi
• A reasoning method for a paraconsistent logic
• CSymLean: A Theorem Prover for the Logic CSL over Symmetric Minspaces

Describes a project that uses

Uses Software

• KEMS

This page was built for publication: Towards an efficient prover for the \(C_1\) paraconsistent logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5170293)