The autoepistemic logic is a
formal logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
for the representation and reasoning of knowledge about knowledge. While
propositional logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
can only express facts, autoepistemic logic can express knowledge and lack of knowledge about facts.
The
stable model semantics The concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure. This is one of several standard approaches to the meaning of negation in logic programming, along with program com ...
, which is used to give a semantics to
logic programming
Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic prog ...
with
negation as failure Negation as failure (NAF, for short) is a non-monotonic inference rule in logic programming, used to derive \mathrm~p (i.e. that ~p is assumed not to hold) from failure to derive ~p. Note that \mathrm ~p can be different from the statement \neg p ...
, can be seen as a simplified form of autoepistemic logic.
Syntax
The
syntax
In linguistics, syntax () is the study of how words and morphemes combine to form larger units such as phrases and sentences. Central concerns of syntax include word order, grammatical relations, hierarchical sentence structure ( constituency) ...
of autoepistemic logic extends that of propositional logic by a
modal operator
A modal connective (or modal operator) is a logical connective for modal logic. It is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non-truth-functional in the following sen ...
[To clarify, the modal operator is a medium white square; this is not a browser rendering issue] 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 Negation as failure (NAF, for short) is a non-monotonic inference rule in logic programming, used to derive \mathrm~p (i.e. that ~p is assumed not to hold) from failure to derive ~p. Note that \mathrm ~p can be different from the statement \neg p ...
.
Semantics
The semantics of autoepistemic logic is based on the ''expansions'' of a theory, which have a role similar to models in
propositional logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
. 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
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional fo ...
, 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.
In terms of
possible world semantics
A possible world is a complete and consistent way the world is or could have been. Possible worlds are widely used as a formal device in logic, philosophy, and linguistics in order to provide a semantics for intensional and modal logic. Their me ...
, an expansion of
consists of an
S5 model of
in which the possible worlds consist only of worlds where
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
and
are tautologies of autoepistemic logic, but not of S5.
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.
Generalizations
In
uncertain inference Uncertain inference was first described by C. J. van Rijsbergen as a way to formally define a query and document relationship in Information retrieval. This formalization is a logical implication with an attached measure of uncertainty.
Definitio ...
, 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 network
A probabilistic logic network (PLN) is a conceptual, mathematical, and computational approach to uncertain inference; inspired by logic programming, but using probabilities in place of crisp (true/false) truth values, and fractional uncertainty in ...
s, 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).)
See also
*
Non-monotonic logic
A non-monotonic logic is a formal logic whose conclusion relation is not monotonic. In other words, non-monotonic logics are devised to capture and represent defeasible inferences (cf. defeasible reasoning), i.e., a kind of inference in which rea ...
*
Modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
Notes
References
*
*
*
*
*
{{refend
Logic programming
Modal logic