The importance of contextual reasoning is emphasized by various researchers in AI. (A partial list includes John McCarthy and his group, R. V. Guha, Yoav Shoham, Giuseppe Attardi and Maria Simi, and Fausto Giunchiglia and his group.) Here, we survey the problem of formalizing context and explore what is needed for an acceptable account of this abstract notion.

In the last decade the concept of context has been extensivelyexploited in many research areas, e.g., distributed artificialintelligence, multi agent systems, distributed databases, informationintegration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion ofcontext have been proposed: Giunchiglia and Serafini's Multi LanguageSystems (ML systems), McCarthy's modal logics of contexts, andGabbay's Labelled Deductive Systems.Previous papers have argued in favor of ML systems with respect to theother approaches. Our aim in this paper is to support these arguments froma (...) theoretical perspective. We provide a very general definition of ML systems, which covers allthe ML systems used in the literature, and we develop a proof theoryfor an important subclass of them: the MR systems. We prove variousimportant results; among other things, we prove a normal form theorem,the sub-formula property, and the decidability of an importantinstance of the class of the MR systems. The paper concludes with a detailed comparison among the alternativeapproaches. (shrink)

Compositional verification aims at managing the complexity of theverification process by exploiting compositionality of the systemarchitecture. In this paper we explore the use of a temporal epistemiclogic to formalize the process of verification of compositionalmulti-agent systems. The specification of a system, its properties andtheir proofs are of a compositional nature, and are formalized within acompositional temporal logic: Temporal Multi-Epistemic Logic. It isshown that compositional proofs are valid under certain conditions.Moreover, the possibility of incorporating default persistence ofinformation in a system, is (...) explored. A completion operation on aspecific type of temporal theories, temporal completion, is introducedto be able to use classical proof techniques in verification withrespect to non-classical semantics covering default persistence. (shrink)

This paper is a contribution to the formalisation of Thagard’s coherence theory. The term coherence is defined as the quality or the state of cohering, especially a logical, orderly, and aesthetically consistent relationship of parts. A coherent set is interdependent such that every element in it contributes to the coherence. We take Thagard’s proposal of a coherence set as that of maximising satisfaction of constraints between elements and explore its use in normative multiagent systems. In particular, we interpret coherence maximisation (...) as a decision-making criterion for norm adoption. We first provide a general coherence framework with the necessary computing tools. Later we introduce a proof-theoretic characterisation of a particular type of coherence, namely the deductive coherence based on Thagard’s principles, and derive a mechanism to compute coherence values between elements in a deductive coherence graph. Our use of graded logic helps us to incorporate reasoning under uncertainty, which is more realistic in the context of multiagent systems. We then conduct a case study where agents deliberate about norm adoption in a multiagent system where there is competition for a common resource. We show how a coherence-maximising agent decides to violate a norm guided by its coherence. (shrink)

Many formalisms for reasoning about knowing commit an agent to be logically omniscient. Logical omniscience is an unrealistic principle for us to use to build a real-world agent, since it commits the agent to knowing infinitely many things. A number of formalizations of knowledge have been developed that do not ascribe logical omniscience to agents. With few exceptions, these approaches are modifications of the possible-worlds semantics. In this paper we use a combination of several general techniques for building non-omniscient reasoners. (...) First we provide for the explicit representation of notions such as problems, solutions, and problem solving activities, notions which are usually left implicit in the discussions of autonomous agents. A second technique is to take explicitly into account the notion of resource when we formalize reasoning principles. We use the notion of resource to describe interesting principles of reasoning that are used for ascribing knowledge to agents. For us, resources are abstract objects. We make extensive use of ordering and inaccessibility relations on resources, but we do not find it necessary to define a metric. Using principles about resources without using a metric is one of the strengths of our approach.We describe the architecture of a reasoner, built from a finite number of components, who solves a puzzle, involving reasoning about knowing, by explicitly using the notion of resource. Our approach allows the use of axioms about belief ordinarily used in problem solving – such as axiom K of modal logic – without being forced to attribute logical omniscience to any agent. In particular we address the issue of how we can use resource-unbounded (e.g., logically omniscient) reasoning to attribute knowledge to others without introducing contradictions. We do this by showing how omniscient reasoning can be introduced as a conservative extension over resource-bounded reasoning. (shrink)

We present a logic-based formalism for modeling ofdialogues between intelligent and autonomous software agents,building on a theory of abstract dialogue games which we present.The formalism enables representation of complex dialogues assequences of moves in a combination of dialogue games, and allowsdialogues to be embedded inside one another. The formalism iscomputational and its modular nature enables different types ofdialogues to be represented.