A 1ST STEP TOWARDS AUTOEPISTEMIC LOGIC PROGRAMMING

Robinson's resolution principle was developed for monotonic classical first order logic. Despite its fundamental place in logic programming, logic programs are generally nonmonotonic in nature. The use of some notion of Negation As Failure (NAF) not only increases the expressive power of logic programs, but it also provides useful means of nonmonotonic reasoning. In this paper, we will first develop a semantics for logic programs and then present a nonmonotonic resolution principle 0 to match the behaviours of nonmonotonic logic programs. The logic that underlies the semantics and the principle is an intensional extension of Levesque's autoepistemic logic. Although this logic is nonmonotonic in nature, it is formalized in classical/standard semantical notions. The 0-resolution principle is a nonmonotonic extension of Konolige's B-resolution for monotonic epistemic logic. It is shown that the principle not only enables us to represent classical negation in the spirit of Minker's disjunctive logic programming paradigm, but it also allows us to represent and reason directly the quantified and nested NAF notions.