Towards an efficient prover for the C₁ paraconsistent logic

DOI10.1016/J.ENTCS.2009.11.007zbMATH Open1291.03020arXiv1202.4144OpenAlexW2066630725MaRDI QIDQ5170293FDOQ5170293

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

Publication date: 23 July 2014

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

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.

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

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

zbMATH Keywords

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Logics of Formal Inconsistency
• The Taming of the Cut. Classical Refutations with Analytic Cut
• A semantical analysis of the calculi \(C_n\)
• Title not available (Why is that?)
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Tableau methods for classical propositional logic
• Title not available (Why is that?)
• A reasoning method for a paraconsistent logic
• Title not available (Why is that?)
• Analytical tableaux for da Costa's hierarchy of paraconsistent logics \(C_n\), \(1\leq n<\omega\)

Cited In (3)

• A reasoning method for a paraconsistent logic
• Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi
• CSymLean: A Theorem Prover for the Logic CSL over Symmetric Minspaces

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)