A Model for Systems of Situated Autonomous Agents: An Application to Automated Deduction

Second International Conference on Multiagent Systems

Volume

Second International Conference on Multiagent Systems

Contents

The goal of this paper is to present a model for systems of situated autonomous agents and to illustrate its application to distributed automated deduction. Our model is based on a sharp distinction between the environment and agent dynamics. In particular, it allows to express how the environment is modified by simultaneously performed actions, to formalize in a very general way the internal activity of an agent in terms of its decision processes (which are based on its own perceptions), and finally to describe the interactions between the agents and the environment, and among themselves. In the application to automated deduction, we integrate our model with the concept of OMRS (open mechanized reasoning system) which distinguishes the logical, the control, and the interaction components of a theorem prover. In this setting, the environment consists of the proof structure, represented as a labelled graph, built when trying to prove a conjecture. The agents, described as OMRS, are situated on the nodes of this graph and act on its nodes and edges (e. g. they may add new nodes). Some experimental results based on a simple example are provided in order to illustrate the potentialities of our approach.