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.
The syntax of autoepistemic logic extends that of propositional logic by a modal operator
This syntax is used for allowing reasoning based on knowledge of facts.
is assumed false if it is not known to be true.
This is a form of negation as failure.
The semantics of autoepistemic logic is based on the expansions of a theory, which have a role similar to model[broken anchor]s in propositional logic.
While a propositional model specifies which atomic propositions are true or false, an expansion specifies which formulae
In particular, the expansions of an autoepistemic formula
make this determination for every subformula
to be treated as a propositional formula, as all its subformulae containing
in this condition can be done using the rules of the propositional calculus.
In order for a specification to be an expansion, it must be that a subformula
has been assigned the value true.
In terms of possible world semantics, an expansion of
[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
are tautologies of autoepistemic logic, but not of S5.
, there is only a single “boxed subformula”, which is
The check for them being actual expansions is as follows.
This result confirms the assumption implicit in
; therefore, the initial assumption that is implicit in
The second one has been regarded as unintuitive, as the initial assumption that
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).)