Soundness and Completeness of a Logic Programming Approach to Default Logic

Nonmonotonic Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 12

Nonmonotonic Reasoning

We present a method of representing some classes of default theories as normal logic programs. The main point is that the standard semantics (i.e. SLDNF-resolution) computes answer substitutions that correspond exactly to the extensions of the represented default theory. We explain the steps of constructing a logic program LogProg(P,D) from a given default theory (P,D), and present the proof ideas of the soundness and completeness results for the approach.