Characterising simple negotiation as distributed agent-based theorem-proving-a preliminary report

Negotiation is a key technique for dynamically organising activity in multi-agent systems, yet the negotiation process itself can often be difficult to reason about. We introduce a framework in which negotiation can be characterised as a form of distributed, multi-agent theorem-proving. Thus, in this preliminary analysis, we show that certain simple forms of negotiation will be successful if, and only if a corresponding theorem can be proved by agents acting as theorem-proving components. We extend this approach further to represent situations where the agent has a choice of possible responses, given a proposal received. In such cases, an ordering strategy is used to select the order in which replies are provided; this corresponds to a common use of ordering within classical theorem-proving