Autoepistemic logic

From Wikipedia, the free encyclopedia

The autoepistemic logic is a formal logic aimed at formalizing representation and reasoning of knowledge about knowledge. While propositional logic can only express facts, autoepistemic logic can express knowledge and lack of knowledge about facts.

The stable model semantics, which is used to give a semantics to logic programming with negation as failure, can be seen as a simplified form of autoepistemic logic.

Contents

[edit] Syntax

The syntax of autoepistemic logic extends that of propositional logic by a modal operator \Box indicating knowledge: if F is a formula, \Box F indicates that F is known. As a result, \Box \neg F indicates that \neg F is known and \neg \Box F indicates that F is not known.

This syntax is used for allowing reasoning based on knowledge of facts. For example, \neg \Box F \rightarrow \neg F means that F is assumed false if it is not known to be true. This is a form of negation as failure.

[edit] Semantics

The semantics of autoepistemic logic is based on the expansions of a theory, which have a role similar to models in propositional logic. While a propositional model specifies which atoms are true or false, an expansion specifies which formulae \Box F are true and which ones are false. In particular, the expansions of an autoepistemic formula T makes this distinction for every subformula \Box F contained in T. This distinction allows T to be treated as a propositional formula, as all its subformulae containing \Box are either true or false. In particular, checking whether T entails F in this condition can be done using the rules of the propositional calculus. In order for an initial assumption to be an expansion, it must be that a subformula F is entailed if and only if \Box F has been initially assumed true.

For example, in the formula T = \Box x \rightarrow x, there is only a single “boxed subformula”, which is \Box x. Therefore, there are only two candidate expansions, assuming it true or false, respectively. The check for them being actual expansions is as follows.

\Box x is false : with this assumption, T becomes tautological, as \Box x \rightarrow x is equivalent to \neg \Box x \vee x, and \neg \Box x is assumed true; therefore, x is not entailed. This result confirms the assumption implicit in \Box x being false, that is, that x is not currently known. Therefore, the assumption that \Box x is false is an expansion.

\Box x is true : together with this assumption, T entails x; therefore, the initial assumption that is implicit in \Box x being true, i.e., that x is known to be true, is satisfied. As a result, this is another expansion.

The formula T has therefore two expansions, one in which x is not known and one in which x is known. The second one has been regarded as unintuitive, as the initial assumption that \Box x is true is the only reason why x is true, which confirms the assumption. In other words, this is a self-supporting assumption. A logic allowing such a self-support of beliefs is called not strongly grounded to differentiate them from strongly grounded logics, in which self-support is not possible. Strongly grounded variants of autoepistemic logic exist.

[edit] See also

[edit] References

  • G. Gottlob (1995). Translating default logic into standard autoepistemic logic. Journal of the ACM, 42:711-740.
  • T. Janhunen (1998). On the intertranslatability of autoepistemic, default and priority logics. In Proceedings of the Sixth European Workshop on Logics in Artificial Intelligence (JELIA'98), pages 216-232.
  • W. Marek and M. Truszczynski (1991). Autoepistemic logic. Journal of the ACM, 38(3):588-619.
  • R. C. Moore (1985). Semantical considerations on nonmonotonic logic. Artificial Intelligence, 25:75-94.
  • I. Niemelä (1988). Decision procedure for autoepistemic logic. In Proceedings of the Ninth International Conference on Automated Deduction (CADE'88), volume 310 of Lecture Notes in Computer Science, pages 675-684. Springer.
Languages