Towards first-order nonmonotonic reasoning

Abstract

We investigate the problem of reasoning in nonmonotonic extensions of first-order logic. In particular, we study reasoning in firstorder MKNF, the modal logic of minimal knowledge and negation as failure introduced by Lifschitz. MKNF can be considered as a unifying framework for several nonmonotonic formalisms, including default logic, autoepistemic logic, circumscription, and logic programming. By suitably extending deduction methods for propositional nonmonotonic logics, we define techniques for reasoning in significant subsets of first-order MKNF, which allow for characterizing decidable fragments of first-order nonmonotonic modal logics. Due to the expressive abilities of MKNF, such techniques can be seen as general reasoning methods for several nonmonotonic formalisms based on first-order logic. We also analyze the relationship between such decidable fragments of MKNF and disjunctive Datalog.