Autoepistemic logic

Autoepistemic logic

The autoepistemic logic is a formal logic aimed at formalizing 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.

yntax

The syntax of autoepistemic logic extends that of propositional logic by a modal operator Box indicating knowledge: if F is a formula, Box F indicates that F is known. As a result, Box eg F indicates that eg F is known and eg Box F indicates that F is not known.

This syntax is used for allowing reasoning based on knowledge of facts. For example, eg Box F ightarrow eg F means that F is assumed false if it is not known to be true. This is a form of negation as failure.

emantics

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 atoms 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, 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.

For example, in the formula T = Box x ightarrow 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 ightarrow x is equivalent to eg Box x vee x, and eg 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.

ee also

* Non-monotonic logic
* Modal logic

References

* G. Gottlob (1995). Translating default logic into standard autoepistemic logic. "Journal of the ACM", 42:711-740.

* T. Janhunen (1998). On the intertranslatability of autoepistemic, default and priority logics. In "Proceedings of the Sixth European Workshop on Logics in Artificial Intelligence (JELIA'98)", pages 216-232.

* W. Marek and M. Truszczynski (1991). Autoepistemic logic. "Journal of the ACM", 38(3):588-619.

* R. C. Moore (1985). Semantical considerations on nonmonotonic logic. "Artificial Intelligence", 25:75-94.

* I. Niemelä (1988). Decision procedure for autoepistemic logic. In "Proceedings of the Ninth International Conference on Automated Deduction (CADE'88)", volume 310 of "Lecture Notes in Computer Science", pages 675-684. Springer.


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Default logic — is a non monotonic logic proposed by Raymond Reiter to formalize reasoning with default assumptions. Default logic can express facts like “by default, something is true”; by contrast, standard logic can only express that something is true or that …   Wikipedia

  • Non-monotonic logic — A non monotonic logic is a formal logic whose consequence relation is not monotonic. Most studied formal logics have a monotonic consequence relation, meaning that adding a formula to a theory never produces a reduction of its set of consequences …   Wikipedia

  • 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… …   Wikipedia

  • Negation as failure — (NAF, for short) is a non monotonic inference rule in logic programming, used to derive (i.e. that is assumed not to hold) from failure to derive . Note that can be different from the statement of the logical negation of …   Wikipedia

  • List of mathematics articles (A) — NOTOC A A Beautiful Mind A Beautiful Mind (book) A Beautiful Mind (film) A Brief History of Time (film) A Course of Pure Mathematics A curious identity involving binomial coefficients A derivation of the discrete Fourier transform A equivalence A …   Wikipedia

  • List of topics in epistemology — * A Defence of Common Sense * A priori and a posteriori (philosophy) * Adaptive representation * Aenesidemus * Aenesidemus (book) * Agrippa the Sceptic * Alison Wylie * Alvin Goldman * Analytic synthetic distinction * Androcentrism * Android… …   Wikipedia

  • Knowledge representation — is an area in artificial intelligence that is concerned with how to formally think , that is, how to use a symbol system to represent a domain of discourse that which can be talked about, along with functions that may or may not be within the… …   Wikipedia

  • Negation as failure — Négation par l échec La négation par l échec (en anglais NAF pour negation as failure, ou NBF pour negation by failure) est une règle d inférence non monotone en programmation logique, utilisée pour la dérivation de à partir de l échec de la… …   Wikipédia en Français

  • Negation by failure — Négation par l échec La négation par l échec (en anglais NAF pour negation as failure, ou NBF pour negation by failure) est une règle d inférence non monotone en programmation logique, utilisée pour la dérivation de à partir de l échec de la… …   Wikipédia en Français

  • Negation par l'echec — Négation par l échec La négation par l échec (en anglais NAF pour negation as failure, ou NBF pour negation by failure) est une règle d inférence non monotone en programmation logique, utilisée pour la dérivation de à partir de l échec de la… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”