Logical Theories for Agent Introspection

Thomas Bolander

AbstractArtificial intelligence systems (agents) generally have models
of the environments they inhabit which they use for representing
facts, for reasoning about these facts and for planning actions. Much
intelligent behaviour seems to involve an ability to model not only
one's external environment but also oneself and one's own
reasoning. We would therefore wish to be able to construct artificial
intelligence systems having such abilities. We call these abilities
introspective. In the attempt to construct agents with
introspective abilities, a number of theoretical problems is
encountered. In
particular, problems related to self-reference make it
difficult to avoid the possibility of such agents performing
self-contradictory reasoning. It is the aim of
this thesis to demonstrate how we can construct agents with
introspective abilities, while at the same time circumventing the problems
imposed by self-reference.

In the standard approach taken in artificial intelligence, the model
that an agent has of its environment is represented as a set of
beliefs. These beliefs are expressed as logical formulas within
a formal, logical theory. When the logical theory is
expressive enough to allow introspective reasoning, the presence of
self-reference causes the theory to be prone to inconsistency. The
challenge therefore becomes to construct logical theories supporting
introspective reasoning while at the same time ensuring that
consistency is retained. In the thesis, we meet this challenge by
devising several such logical theories which we prove to be
consistent. These theories are all based on first-order predicate
logic.

To prove our consistency results, we develop a general mathematical
framework, suitable for proving a large number of consistency results
concerning logical theories involving various kinds of reflection. The
principal idea of the framework is to relate self-reference and other
problems involved in introspection to properties of certain
kinds of graphs. These are graphs representing the semantical
dependencies among the logical sentences. The framework is mainly
inspired by developments within semantics for logic programming within
computational logic and formal theories of truth within philosophical
logic.

The thesis provides a number of examples showing how the developed
theories can be used as reasoning frameworks for agents with
introspective abilities.
TypePh.D. thesis [Academic thesis]
Year2003
PublisherInformatics and Mathematical Modelling (IMM), Technical University of Denmark
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering