Programming in Autoepistemic Logic

Abstract

We propose a language for programming in autoepistemic logic that extends the standard logic programming and incorporates incomplete information. By syntactically distinguishing the true negation from the lack of information, we also provide a way to define negative information explicitly. A fixpoint semantics can be defined for stratified and conservative programs. In this paper, we investigate definite autoepistemic programs. We investigate fixpoints of definite autoepistemic programs and show that they coincide with the declarative semantics of these programs. We also define a resolution procedure, called SLSAE-resolution, for such programs. SLSAE-resolution is sound and complete for stratified, conservative, and solvable programs.