Autoepistemic Logic
   HOME

TheInfoList



OR:

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 ...
\BoxTo clarify, the modal operator \Box is a medium white square; this is not a browser rendering issue indicating knowledge: if F is a formula, \Box F indicates that F is known. As a result, \Box \neg F indicates that \neg F is known and \neg \Box F indicates that F is not known. This syntax is used for allowing reasoning based on knowledge of facts. For example, \neg \Box F \rightarrow \neg F means that F 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 \Box F are true and which ones are false. In particular, the expansions of an autoepistemic formula T makes this distinction for every subformula \Box F contained in T. This distinction allows T 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 \Box are either true or false. In particular, checking whether T entails 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 is entailed if and only if \Box F 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 T consists of an S5 model of T in which the possible worlds consist only of worlds where T 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 \neg \Box p and \neg \Box \neg p are tautologies of autoepistemic logic, but not of S5. For example, in the formula T = \Box x \rightarrow x, there is only a single “boxed subformula”, which is \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. \Box x is false : with this assumption, T becomes tautological, as \Box x \rightarrow x is equivalent to \neg \Box x \vee x, and \neg \Box x is assumed true; therefore, x is not entailed. This result confirms the assumption implicit in \Box x being false, that is, that x is not currently known. Therefore, the assumption that \Box x is false is an expansion. \Box x is true : together with this assumption, T entails x; therefore, the initial assumption that is implicit in \Box x being true, i.e., that x is known to be true, is satisfied. As a result, this is another expansion. The formula T has therefore two expansions, one in which x is not known and one in which x is known. The second one has been regarded as unintuitive, as the initial assumption that \Box x is true is the only reason why x 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