@PHDTHESIS\{IMM2003-02825,
    author       = "T. Bolander",
    title        = "Logical Theories for Agent Introspection",
    year         = "2003",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Professor J{\o}rgen Fischer Nilsson",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/2825-full.html",
    abstract     = "Artificial 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.

In Danish:

Intelligente systemer (agenter) er generelt udstyret med en model af de omgivelser de befinder sig i. De bruger denne model til at repr{\ae}sentere egenskaber ved omgivelserne, til at r{\ae}ssonere omkring disse egenskaber og til at planl{\ae}gge handlinger. En overvejende del af det vi s{\ae}dvanligvis opfatter som intelligent handlem{\aa}de synes at involvere en evne til ikke kun at modellere ens ydre omgivelser, men ogs{\aa} at modellere sig selv og ens egen r{\ae}ssonering. Vi {\o}nsker derfor at v{\ae}re i stand til at konstruere intelligente systemer som har s{\aa}danne evner. Disse evner kaldes introspektive. I fors{\o}get p{\aa} at konstruere agenter med introspektive evner st{\o}der man p{\aa} en del problemer af teoretisk natur. I s{\ae}rdeleshed st{\o}der man p{\aa} problemer relateret til selvreference, som g{\o}r det vanskeligt at sikre sig mod at s adanne agenter kan foretage selvmodsigende r{\ae}ssonementer. M{\aa}let med denne afhandling er at vise hvordan vi kan konstruere agenter med introspektive evner p{\aa} en s{\aa}dan m{\aa}de at problemerne omkring selvreference omg{\aa}s.

Den model en agent har af sine omgivelser lader man s{\ae}dvanligvis repr{\ae}sentere ved en m{\ae}ngde af s{\ae}tninger, der udtrykker de forestillinger som agenten har om verden. Disse s{\ae}tninger formuleres indenfor en formel, logisk teori. Hvis denne logiske teori har tilstr{\ae}kkelig udtrykskraft til at at tillade introspektiv r{\ae}ssonering, vil tilstedev{\ae}relsen af selvreference i de fleste tilf{\ae}lde for{\aa}rsage at teorien bliver inkonsistent. Udfordringen kommer derfor til at best{\aa} i at  finde m{\aa}der at konstruere logiske teorier p{\aa} som underst{\o}tter introspektiv r{\ae}ssonering, men hvor konsistens samtidig er sikret. I afhandlingen im{\o}dekommer vi denne udfordring ved at konstruere flere s{\aa}danne logiske teorier, som vi beviser at v{\ae}re konsistente. Disse teorier er alle baseret p{\aa} f{\o}rste-ordens pr{\ae}dikatlogik.

I forbindelse med vores konsistensresultater udvikler vi et generelt matematisk v{\ae}rkt{\o}j, som kan benyttes til at bevise konsistensen af en lang r{\ae}kke logiske teorier involverende forskellige former for re eksion. Den b{\ae}rende ide i dette v{\ae}rkt{\o}j er at relatere selvreference|og andre af problemerne involveret i introspektion - til egenskaber ved bestemte typer af grafer. Dette er grafer som repr{\ae}senterer de semantiske afh{\ae}ngigheder imellem s{\ae}tningerne i de p{\aa}g{\ae}ldende teorier. V{\ae}rkt{\o}jet er inspireret af tilsvarende v{\ae}rkt{\o}jer udviklet i forbindelse med semantikker for logik-programmer indenfor datalogisk logik og formelle teorier for sandhed indenfor filosofisk logik.

Afhandlingen giver et antal eksempler p{\aa} hvordan de udviklede teorier kan anvendes som fundament for agenter med introspektive evner."
}