Stratification and Tractability in Nonmonotonic Reasoning

Reference:

Jussi Rintanen. Stratification and tractability in nonmonotonic reasoning. Research Report A20, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland, November 1992.

Abstract:

Knowledge-based systems use forms of reasoning that do not satisfy the monotonicity property of classical logical reasoning. Therefore, several nonmonotonic logics have been developed for the investigation of theoretical foundations of knowledge-based systems. This work investigates efficient inference procedures for knowledge representation using the framework of nonmonotonic logics. Recent results show that nonmonotonic reasoning cannot be brought to tractable level by restricting merely the form of the formulae. In this work the impact of the structural property of stratification on the complexity of nonmonotonic reasoning is investigated. Autoepistemic logic is used as the framework for establishing the results, because several other nonmonotonic formalisms can be embedded in it. The main result of the work is that in stratified cases the complexity of nonmonotonic reasoning is approximately the same as that of corresponding classical monotonic reasoning. This is shown by giving a general decision procedure for stratified autoepistemic theories and analyzing its complexity with respect to the complexity of the classical theorem-proving required. It turns out that for theories for which the classical theorem-proving is polynomial time, also the decision procedure runs in polynomial time. As an example of this, two tractable classes of autoepistemic theories based on the Horn clause subset of propositional logic are presented. Also the implications of these results on the complexity of reasoning in default logic, truth-maintenance systems, and propositional logic programs are discussed.

Keywords:

nonmonotonic reasoning, autoepistemic logic, tractability, stratification

Suggested BibTeX entry:

@techreport{HUT-TCS-A20,
    address = {Espoo, Finland},
    author = {Jussi Rintanen},
    institution = {Helsinki University of Technology, Digital Systems Laboratory},
    month = {November},
    number = {A20},
    pages = {71},
    title = {Stratification and Tractability in Nonmonotonic Reasoning},
    type = {Research Report},
    year = {1992},
}