A logic for reasoning with inconsistency

Most known computational approaches to reasoning have problems when facing inconsistency, so they assume that a given logical system is consistent. Unfortunately, the latter is difficult to verify and very often is not true. It may happen that addition of data to a large system makes it inconsistent, and hence destroys the vast amount of meaningful information. We present a logic, called APC (annotated predicate calculus; cf. annotated logic programs of 4, 5]), that treats any set of clauses, either consistent or not, in a uniform way. In this logic, consequences of a contradiction are not nearly as damaging as in the standard predicate calculus, and meaningful information can still be extracted from an inconsistent set of formulae. APC has a resolution-based sound and complete proof procedure. We also introduce a novel notion of epistemic entailment and show its importance for investigating inconsistency in predicate calculus as well as its application to nonmonotonic reasoning. Most importantly, our claim that a logical theory is an adequate model of human perception of inconsistency, is actually backed by rigorous arguments.A preliminary report on this research appeared in LICS'89.Work of M. Kifer was supported in part by the NSF grants DCR-8603676, IRI-8903507.Work of E. L. Lozinskii was supported in part by Israel National Council for Research and Development under the grants 2454-3-87, 2545-2-87, 2545-3-89 and by Israel Academy of Science, grant 224-88.