Abstract
Providing a logical characterisation of rational agent reasoning has been a long standing challenge in artificial intelligence (AI) research. It is a challenge that is not only of interest for the construction of AI agents, but is of equal importance in the modelling of agent behaviour. The goal of this thesis is to contribute to the formalisation of agent reasoning by showing that the computational limitations of agents is a vital component of modelling rational behaviour. To achieve this aim, both motivational and formal aspects of resource-bounded agents are examined.
It is a central argument of this thesis that accounting for computational limitations is critical to the success of agent reasoning, yet has received only limited attention from the broader research community. Consequently, an important contribution of this thesis is in its advancing of motivational arguments in support of the need to account for computational limitations in agent reasoning research.
As a natural progression from the motivational arguments, the majority of this thesis is devoted to an examination of propositional approximate logics. These logics represent a step towards the development of resource-bounded agents, but are also applicable to other areas of automated reasoning.
This thesis makes a number of contributions in mapping the space of approximate logics. In particular, it draws a connection between approximate logics and knowledge compilation, by developing an approximate knowledge compilation method based on Cadoli and Schaerf’s S-3 family of approximate logics. This method allows for the incremental compilation of a knowledge base, thus reducing the need for a costly recompilation process. Furthermore, each approximate compilation has well-defined logical properties due to its correspondence to a particular S-3 logic. Important contributions are also made in the examination of approximate logics for clausal reasoning. Clausal reasoning is of particular interest due to the efficiency of modern clausal satisfiability solvers and the related research into problem hardness. In particular, Finger's Logics of Limited Bivalence are shown to be applicable to clausal reasoning. This is subsequently shown to logically characterise the behaviour of the well-known DPLL algorithm for determining boolean satisfiability, when subjected to restricted branching.