The autoepistemic logic is a formal logic for the 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 syntax of autoepistemic logic extends that of propositional logic by a modal operator indicating knowledge: if is a formula, indicates that is known. As a result, indicates that is known and indicates that is not known.
This syntax is used for allowing reasoning based on knowledge of facts. For example, means that is assumed false if it is not known to be true. This is a form of negation as failure.
To clarify, the modal operator actually is a medium white square, and is not a browser rendering issue.
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 axioms are true or false, an expansion specifies which formulae are true and which ones are false. In particular, the expansions of an autoepistemic formula makes this distinction for every subformula contained in . This distinction allows to be treated as a propositional formula, as all its subformulae containing are either true or false. In particular, checking whether entails 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 is entailed if and only if has been initially assumed true.
For example, in the formula , there is only a single “boxed subformula”, which is . Therefore, there are only two candidate expansions, assuming it true or false, respectively. The check for them being actual expansions is as follows.
is false : with this assumption, becomes tautological, as is equivalent to , and is assumed true; therefore, is not entailed. This result confirms the assumption implicit in being false, that is, that is not currently known. Therefore, the assumption that is false is an expansion.
is true : together with this assumption, entails ; therefore, the initial assumption that is implicit in being true, i.e., that is known to be true, is satisfied. As a result, this is another expansion.
The formula has therefore two expansions, one in which is not known and one in which is known. The second one has been regarded as unintuitive, as the initial assumption that is true is the only reason why 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.
In uncertain inference, the known/unknown duality of truth values is replaced by a degree of certainty of a fact or deduction; certainty may vary from 0 (completely uncertain/unknown) to 1 (certain/known). In probabilistic logic networks, truth values are also given a probabilistic interpretation (i.e. truth values may be uncertain, and, even if almost certain, they may still be "probably" true (or false).)
- Gottlob, G. (July 1995). "Translating default logic into standard autoepistemic logic". Journal of the ACM 42 (4): 711–740. doi:10.1145/210332.210334.
- Janhunen, T. (1998). "On the intertranslatability of autoepistemic, default and priority logics". In Dix, Jürgen; del Cerro, Luís Fariñas; Furbach, Ulrich. Logics in Artificial Intelligence: European Workshop, JELIA '98, Dagstuhl, Germany, October 12–15, 1998 : Proceedings. Lecture Notes in Computer Science: Lecture notes in artificial intelligence. Springer. pp. 216–232. ISBN 3540495452.
- Marek, W.; Truszczyński, M. (July 1991). "Autoepistemic logic". Journal of the ACM 38 (3): 588–618. doi:10.1145/116825.116836.
- Moore, R.C. (January 1985). "Semantical considerations on nonmonotonic logic". Artificial Intelligence 25: 75–94. doi:10.1016/0004-3702(85)90042-6.
- Niemelä, I. (1988). "Decision procedure for autoepistemic logic". In Lusk, Ewing; Overbeek, Ross. 9th International Conference on Automated Deduction: Argonne, Illinois, USA, May 23-26, 1988. Proceedings. Lecture Notes in Computer Science 310. Springer. pp. 675–684. ISBN 978-3-540-19343-2.