Automatic theorem proving in paraconsistent logics: Theory and implementation

Newton C.A. Da Costa, Lawrence Joseph Henschen, James J. Lu, V. S. Subrahmanian

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Scopus citations


Databases and knowledge bases may be inconsistent in many ways. However, a database that is inconsistent may, nonetheless, contain a great deal of useful information. Classical logic, however, would deem such a database as useless. Paraconsistent logics are a family of logics introduced by da Costa. A family of paraconsistent logics called annotated logics were proposed by Subrahmanian in [17]. Subsequently, these logics found use in reasoning about logic programs that contained inconsistent and/or erroneous information, as well as in the study of inheritance hierarchies and object oriented databases. However, no full-fledged study of automatic theorem proving in these logics has been carried out to date. In this paper, we develop a linear resolution style proof procedure for mechanical reasoning in these paraconsistent logics.

Original languageEnglish (US)
Title of host publication10th International Conference on Automated Deduction, Proceedings
EditorsMark E. Stickel
PublisherSpringer Verlag
Number of pages15
ISBN (Print)9783540528852
StatePublished - Jan 1 1990
Event10th International Conference on Automated Deduction, CADE 1990 - Kaiserslautern, Germany
Duration: Jul 24 1990Jul 27 1990

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume449 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other10th International Conference on Automated Deduction, CADE 1990

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Automatic theorem proving in paraconsistent logics: Theory and implementation'. Together they form a unique fingerprint.

Cite this