ⓘ 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.
1. Syntax
The syntax of autoepistemic logic extends that of propositional logic by a modal operator ◻ {\displaystyle \Box } indicating knowledge: if F {\displaystyle F} is a formula, ◻ F {\displaystyle \Box F} indicates that F {\displaystyle F} is known. As a result, ◻ ¬ F {\displaystyle \Box \neg F} indicates that ¬ F {\displaystyle \neg F} is known and ¬ ◻ F {\displaystyle \neg \Box F} indicates that F {\displaystyle F} is not known.
This syntax is used for allowing reasoning based on knowledge of facts. For example, ¬ ◻ F → ¬ F {\displaystyle \neg \Box F\rightarrow \neg F} means that F {\displaystyle F} is assumed false if it is not known to be true. This is a form of negation as failure.
2. 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 ◻ F {\displaystyle \Box F} are true and which ones are false. In particular, the expansions of an autoepistemic formula T {\displaystyle T} makes this distinction for every subformula ◻ F {\displaystyle \Box F} contained in T {\displaystyle T}. This distinction allows T {\displaystyle T} to be treated as a propositional formula, as all its subformulae containing ◻ {\displaystyle \Box } are either true or false. In particular, checking whether T {\displaystyle T} entails F {\displaystyle 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 {\displaystyle F} is entailed if and only if ◻ F {\displaystyle \Box F} has been initially assumed true.
In terms of possible world semantics, an expansion of T {\displaystyle T} consists of an S5 model of T {\displaystyle T} in which the possible worlds consist only of worlds where T {\displaystyle T} is true. Thus, autoepistemic logic extends S5 ; the extension is proper, since ¬ ◻ p {\displaystyle \neg \Box p} and ¬ ◻ ¬ p {\displaystyle \neg \Box \neg p} are tautologies of autoepistemic logic, but not of S5.
For example, in the formula T = ◻ x → x {\displaystyle T=\Box x\rightarrow x}, there is only a single" boxed subformula”, which is ◻ x {\displaystyle \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.
◻ x {\displaystyle \Box x} is false: with this assumption, T {\displaystyle T} becomes tautological, as ◻ x → x {\displaystyle \Box x\rightarrow x} is equivalent to ¬ ◻ x ∨ x {\displaystyle \neg \Box x\vee x}, and ¬ ◻ x {\displaystyle \neg \Box x} is assumed true; therefore, x {\displaystyle x} is not entailed. This result confirms the assumption implicit in ◻ x {\displaystyle \Box x} being false, that is, that x {\displaystyle x} is not currently known. Therefore, the assumption that ◻ x {\displaystyle \Box x} is false is an expansion.
◻ x {\displaystyle \Box x} is true: together with this assumption, T {\displaystyle T} entails x {\displaystyle x} ; therefore, the initial assumption that is implicit in ◻ x {\displaystyle \Box x} being true, i.e., that x {\displaystyle x} is known to be true, is satisfied. As a result, this is another expansion.
The formula T {\displaystyle T} has therefore two expansions, one in which x {\displaystyle x} is not known and one in which x {\displaystyle x} is known. The second one has been regarded as unintuitive, as the initial assumption that ◻ x {\displaystyle \Box x} is true is the only reason why x {\displaystyle x} is true, which confirms the assumption. In other words, this is a selfsupporting assumption. A logic allowing such a selfsupport of beliefs is called not strongly grounded to differentiate them from strongly grounded logics, in which selfsupport is not possible. Strongly grounded variants of autoepistemic logic exist.
3. 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)

Knowledge 

History of knowledge 
Outline of knowledge 
A Causal Theory of Knowing 

Knowledge acquisition 

Activity theory 

Age of Enlightenment 
Agnotology 
Arationality 

Knowledge ark 

Bildung 

Body of knowledge 

Book desert 
Cognitive closure (philosophy) 
Cognitive justice 

Common knowledge 
Common knowledge (logic) 

Community of practice 

Creative computing 

Credential 
Democratization of knowledge 

Descriptive knowledge 
Discernment 
Dispersed knowledge 

Distributed knowledge 
Knowledge divide 

Domain knowledge 

Encyclopedic knowledge 

Knowledge enterprise 

Knowledge environment 

Episteme 
Experiential knowledge 

Expert 
Explicit knowledge 

Knowledge extraction 
Faith literate 

Foolishness 

Forbidden knowledge 
Foreknowledge 

Functional illiteracy 

General knowledge 
Gettier problem 

Growth of knowledge 
Halflife of knowledge 

Ignorance 
Inert knowledge 

Informality 
Institutional memory 

Intellectualism 

Film 

Television show 

Game 

Sport 

Science 

Hobby 

Travel 

Technology 

Brand 

Outer space 

Cinematography 

Photography 

Music 

Literature 

Theatre 

History 

Transport 

Visual arts 

Recreation 

Politics 

Religion 

Nature 

Fashion 

Subculture 

Animation 

Award 

Interest 