Summary
In this paper we present an effective prover for mbC, a minimal inconsistency logic. The mbC logic is a paraconsistent logic of the family of logics of formal inconsistency. Paraconsistent logics have several philosophical motivations as well as many applications in Artificial Intelligence such as in belief revision, inconsistent knowledge reasoning, and logic programming. We have implemented the KEMS prover for mbC, a theorem prover based on the KE tableau method for mbC. We show here that the proof system on which this prover is based is sound, complete and analytic. To evaluate the KEMS prover for mbC, we devised four families of mbC-valid formulas and we present here the first benchmark results using these families.
Chapter PDF
References
H. A. Blair and V. S. Subrahmanian. Paraconsistent logic programming. Theor. Comput. Sci., 68(2):135–154, 1989.
Carlos Caleiro, Walter Carnielli, Marcelo E. Coniglio, and Joao Marcos. Two’s company: “The humbug of many logical values”. In Logica Universalis, pages 169–189. Birkhäuser Verlag, Basel, Switzerland, 2005.
Walter Carnielli, Marcelo E. Coniglio, and Joao Marcos. Logics of Formal Inconsistency. In Handbook of Philosophical Logic, volume 12. Kluwer Academic Publishers, 2005.
Newton C. A. da Costa, Lawrence J. Henschen, James J. Lu, and V. S. Subrahmanian. Automatic theorem proving in paraconsistent logics: theory and implementation. In CADE-10: Proceedings of the tenth international conference on Automated deduction, pages 72–86, New York, NY, USA, 1990. Springer-Verlag New York, Inc.
Newton C. A. da Costa, Décio Krause, and Otávio Bueno. Paraconsistent logics and paraconsistency: Technical and philosophical developments. CLE e-prints (Section Logic), 4(3), 2004.
Marcello D’Agostino. Tableau methods for classical propositional logic. In Marcello D’Agostino et al., editor, Handbook of Tableau Methods, chapter 1, pages 45–123. Kluwer Academic Press, 1999.
Marcello D’Agostino and Marco Mondadori. The taming of the cut: Classical refutations with analytic cut. Journal of Logic and Computation, pages 285–319, 1994.
Sandra de Amo, Walter Alexandre Carnielli, and Joao Marcos. A logical frame-work for integrating inconsistent information in multiple databases. In FoIKS’ 02: Proceedings of the Second International Symposium on Foundations of Information and Knowledge Systems, pages 67–84, London, UK, 2002. Springer-Verlag.
Itala M. Loffredo D’Ottaviano and Milton Augustinis de Castro. Analytical Tableaux for da Costa’s Hierarchy of Paraconsistent Logics C n, 1 ≤ n ≤ ω). Journal of Applied Non-Classical Logics, 15(l):69–103, 2005.
Adolfo Gustavo Serra Seca Neto. KEMS-A KE-based Multi-Strategy Theorem Prover, 2006. Retrieved February 01, 2006, from http://gsd.ime.usp.br/~adolfo/projetos/KEMS.zip.
Adolfo Gustavo Serra Seca Neto and Marcelo Finger. Implementing a multi-strategy theorem prover. In Ana Cristina Bicharra Garcia and Fernando Santos Osório, editors, Proceedings of the V ENIA, São Leopoldo-RS, Brazil, July 22–29 2005, 2005.
G. Priest. Paraconsistent Belief Revision. Theoria, 67:214–228, 2001.
Raymond M. Smullyan. First-Order Logic. Springer-Verlag, 1968.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 International Federation for Information Processing
About this paper
Cite this paper
Neto, A.G.S.S., Finger, M. (2006). Effective Prover for Minimal Inconsistency Logic. In: Bramer, M. (eds) Artificial Intelligence in Theory and Practice. IFIP AI 2006. IFIP International Federation for Information Processing, vol 217. Springer, Boston, MA . https://doi.org/10.1007/978-0-387-34747-9_48
Download citation
DOI: https://doi.org/10.1007/978-0-387-34747-9_48
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-34654-0
Online ISBN: 978-0-387-34747-9
eBook Packages: Computer ScienceComputer Science (R0)