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.

1 Syntax
2 Semantics
3 See also
4 References

[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.

Retrieved from "http://en.wikipedia.org../../../a/u/t/Autoepistemic_logic.html"

Category: Logic in computer science