Multi-Agent Reasoning with Belief Contexts III: Towards the Mechanization

As discussed in previous papers, belief contexts are a powerful and adequate formalism for the representation of propositional attitudes in a multiagent environment. Belief contexts give also implementational advantages. In this paper we discuss the issues related to the practical use of belief contexts, by showing the mechanized solution to some paradigmatic case studies. We show that this mechanization has the following implementational advantages. First, proofs have a natural interpretation, close to standard patterns in reasoning about propositional attitudes, and are based only on few conceptual reasoning steps: this makes proof search easier to understand and automatize. Furthermore, it is easier to implement inference strategies which exploit the structure of the problem. Finally, substantial parts of reasoning are local to contexts: this allows for the efficient use of general purpose decider