Distributed problem-solving as concurrent theorem proving

Our principal aim in this paper is to demonstrate that distributed problem solving may fruitfully be viewed as concurrent theorem proving. We begin by introducing a novel agent-based approach to concurrent theorem proving, and then describe Concurrent METATEM, a multi-agent programming language whose model of computation is closely related to that used within the theorem proving approach. An extended case study is then presented, wherein we demonstrate how a multi-agent planning system can be implemented within the agent-based theorem proving framework. We then show how extensions and refinements of the planning system can easily be accommodated within this framework. We conclude with a detailed discussion of related work, from both the multi-agent systems community and the (concurrent) theorem proving community.