Autoepistemic logic

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 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.
Syntax.
The syntax of autoepistemic logic extends that of propositional logic by a modal operator formula_1 indicating knowledge: if formula_2 is a formula, formula_3 indicates that formula_2 is known. As a result, formula_5 indicates that formula_6 is known and formula_7 indicates that formula_2 is not known.
This syntax is used for allowing reasoning based on knowledge of facts. For example, formula_9 means that formula_2 is assumed false if it is not known to be true. This is a form of negation as failure.
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 axioms are true or false, an expansion specifies which formulae formula_3 are true and which ones are false. In particular, the expansions of an autoepistemic formula formula_12 makes this distinction for every subformula formula_3 contained in formula_12. This distinction allows formula_12 to be treated as a propositional formula, as all its subformulae containing formula_1 are either true or false. In particular, checking whether formula_12 entails formula_2 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 formula_2 is entailed if and only if formula_3 has been initially assumed true.
In terms of possible world semantics, an expansion of formula_12 consists of an S5 model of formula_12 in which the possible worlds consist only of worlds where formula_12 is true. [The possible worlds need not contain all such consistent worlds; this corresponds to the fact that modal propositions are assigned truth values before checking derivability of the ordinary propositions.] Thus, autoepistemic logic extends S5; the extension is proper, since formula_24 and formula_25 are tautologies of autoepistemic logic, but not of S5.
For example, in the formula formula_26, there is only a single “boxed subformula”, which is formula_27. Therefore, there are only two candidate expansions, assuming it true or false, respectively. The check for them being actual expansions is as follows.
formula_27 is false : with this assumption, formula_12 becomes tautological, as formula_30 is equivalent to formula_31, and formula_32 is assumed true; therefore, formula_33 is not entailed. This result confirms the assumption implicit in formula_27 being false, that is, that formula_33 is not currently known. Therefore, the assumption that formula_27 is false is an expansion.
formula_27 is true : together with this assumption, formula_12 entails formula_33; therefore, the initial assumption that is implicit in formula_27 being true, i.e., that formula_33 is known to be true, is satisfied. As a result, this is another expansion.
The formula formula_12 has therefore two expansions, one in which formula_33 is not known and one in which formula_33 is known. The second one has been regarded as unintuitive, as the initial assumption that formula_27 is true is the only reason why formula_33 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.
Generalizations.
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).)