A decision method for nonmonotonic reasoning based on autoepistemic reasoning

    Research output: Contribution to journalArticleScientificpeer-review

    6 Citations (Scopus)

    Abstract

    A novel decision method for autoepistemic reasoning is developed and proved correct. The method is applicable in a general setting, i.e., for an autoepistemic logic based on a given classical logic. It provides a decision procedure for a tightly grounded form of autoepistemic reasoning based on L-hierarchic expansions as well as for autoepistemic reasoning based on Moore-style expansions and N-expansions. Prominent formalizations of nonmonotonic reasoning, such as default logic and circumscription, can be embedded into autoepistemic logic based on L-hierarchic expansions using simple local translations. Hence, the method can serve as a unified reasoning tool for a wide range of forms of nonmonotonic reasoning. The method is conceptually simple, and the inherent sources of complexity and targets for optimization are clearly identifiable. As an example of exploiting optimization possibilities, a new decision method for Reiter's default logic is developed where ideas from autoepistemic reasoning are used to prune the search space for applicable default rules when constructing extensions of a default theory.

    Original languageEnglish
    Pages (from-to)3-42
    Number of pages40
    JournalJournal of Automated Reasoning
    Volume14
    Issue number1
    DOIs
    Publication statusPublished - Feb 1995
    MoE publication typeA1 Journal article-refereed

    Keywords

    • AUTOMATED THEOREM PROVING
    • AUTOEPISTEMIC LOGIC
    • DEFAULT LOGIC
    • DEFAULT
    • LOGIC

    Cite this