ML systems: A Proof Theory for Contexts

In the last decade the concept of context has been extensively exploited in many research areas, e.g., distributed artificial intelligence, multi agent systems, distributed databases, information integration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion of context have been proposed: Giunchiglia and Serafini's Multi Language Systems (ML systems), McCarthy's modal logics of contexts, and Gabbay's Labelled Deductive Systems. Previous papers have argued in favor of ML systems with respect to the other approaches. Our aim in this paper is to support these arguments from a theoretical perspective. We provide a very general definition of ML systems, which covers all the ML systems used in the literature, and we develop a proof theory for an important subclass of them: the MR systems. We prove various important results; among other things, we prove a normal form theorem, the sub-formula property, and the decidability of an important instance of the class of the MR systems. The paper concludes with a detailed comparison among the alternative approaches.