TY - GEN
T1 - Automatic theorem proving in paraconsistent logics
T2 - 10th International Conference on Automated Deduction, CADE 1990
AU - Da Costa, Newton C.A.
AU - Henschen, Lawrence Joseph
AU - Lu, James J.
AU - Subrahmanian, V. S.
N1 - Publisher Copyright:
© Springer-Veflag Berlin Heidelberg 1990.
PY - 1990
Y1 - 1990
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84887121634&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84887121634&partnerID=8YFLogxK
U2 - 10.1007/3-540-52885-7_80
DO - 10.1007/3-540-52885-7_80
M3 - Conference contribution
AN - SCOPUS:84887121634
SN - 9783540528852
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 72
EP - 86
BT - 10th International Conference on Automated Deduction, Proceedings
A2 - Stickel, Mark E.
PB - Springer Verlag
Y2 - 24 July 1990 through 27 July 1990
ER -