Catálogo de publicaciones - libros

If we are to take the notion of speech act seriously, we must be able to treat speech acts as acts. In this paper, we will try to model changes brought about by various acts of commanding in terms of a variant of update logic. We will combine a multi-agent variant of the language of monadic deontic logic with a dynamic language to talk about the situations before and after the issuance of commands, and the commands that link those situations. Although the resulting logic inherits various inadequacies from monadic deontic logic, some interesting principles are captured and seen to be valid nonetheless. A complete axiomatization and some interesting valid principles together with concrete examples will be presented, and suggestions for further research will be made.

We present a multi-agent formalism based on extended answer set programming. The system consists of independent agents connected via a communication channel, where knowledge and beliefs of each agent are represented by a logic program. When presented with an input set of literals from its predecessor, an agent computes its output as an extended answer set of its program enriched with the input, carefully eliminating contradictions that might occur.

It turns out that while individual agents are rather simple, the interaction strategy makes the system quite expressive: essentially a hierarchy of a fixed number of agents captures the complexity class , i.e. the -th level of the polynomial hierarchy. Furthermore, unbounded hierarchies capture the polynomial hierarchy . This makes the formalism suitable for modelling complex applications of MAS, for example cooperative diagnosis. Furthermore, such systems can be realized by implementing an appropriate control strategy on top of existing solvers such as and .

In this paper, we discuss the dynamics of multi-agent belief change in the framework of linear algebra. We regard an epistemic state of each agent as an element in the vector space spanned by the basis of possible worlds, so that belief change corresponds to a linear transformation on this vector space. The compound belief states of multi-agents are treated by using the product tensor of the vector for each agent. In this formulation, the reasoning in the process of belief change can be reduced to the matrix and tensor calculation.

It is recognised that institutions are potentially powerful means for making agent interactions effective and efficient, but institutions will only really be useful when, as in other safety-critical scenarios, it is possible to prove that particular properties do or do not hold for all possible encounters. In contrast to symbolic model-checking, answer set programming permits the statement of problems and queries in domain-specific terms as executable logic programs, thus eliminating the gap between specification and verification language. Furthermore, results are presented in the same terms. In this paper we describe the use of answer set programs as an institutional modelling technique. We demonstrate that our institutional model can be intuitively be mapped into an answer set program such that the ordered event traces of the former can be obtained as the answer sets of the latter, allowing for an easy way to query properties of models.

In this paper, we propose the logic for reasoning about probabilistic belief, called . Our language includes formulas that essentially express “agent believes that the probability of is at least ”. We first provide an inference system of , and then introduce a probabilistic semantics for . The soundness and finite model property of are proven.

This paper presents an implementation of (a simplified version of) the cognitive agent programming language 3APL in the Maude term rewriting language. Maude is based on the mathematical theory of rewriting logic. The language has been shown to be suitable both as a logical framework in which many other logics can be represented, and as a semantic framework, through which programming languages with an operational semantics can be implemented in a rigorous way. We explore the usage of Maude in the context of agent programming languages, and argue that, since agent programming languages such as 3APL have both a logical and a semantic component, Maude is very well suited for prototyping such languages. Further, we show that, since Maude is reflective, 3APL’s meta-level reasoning cycle or deliberation cycle can be implemented very naturally in Maude. Moreover, although we have implemented a simplified version of 3APL, we argue that Maude is very well suited for implementing various extensions of this implemented version. An important advantage of Maude, besides the fact that it is well suited for prototyping agent programming languages, is that it can be used for verification as it comes with an LTL model checker. Although this paper does not focus on model checking 3APL, the fact that Maude provides these verification facilities is an important motivation for our effort of implementing 3APL in Maude.

In this paper, we will show that theory-based legal argumentation can be formalized as a dialogue game tree. In [37], a variation of Olsson’s additive consolidation [29] is used for the formalization, but this dialogue game was not treed, because, in each move on the dialogue, the consolidation must construct a unique coherent theory, but not several coherent theories. Therefore, we abandon the requirement that rational consolidation must be unique, and we allow the consolidation to generate plural outputs. Such an operator will be applied for a dialogue game tree with Bench-Capon and Sartor’s example.

In this paper, we present a temporal epistemic logic, called , which generalizes -calculus by introducing knowledge modality and cooperation modality. Similar to -calculus, is a succinct and expressive language. It is showed that temporal modalities such as “always”, “sometime” and “until”, and knowledge modalities such as “everyone knows” and “common knowledge” can be expressed in such a logic. Furthermore, we study the model checking technique and its complexity. Finally, we use and its model checking algorithm to study the well-known trains and controller problem.

In this paper we develop a semantics of our approach based on commitments and arguments for conversational agents. We propose a logical model based on CTL* (Extended Computation Tree Logic) and on dynamic logic. Called Commitment and Argument Network (CAN), our formal framework based on this hybrid approach uses three basic elements: social commitments, actions that agents apply to these commitments and arguments that agents use to support their actions. The advantage of this logical model is to gather all these elements and the existing relations between them within the same framework. The semantics we develop here enables us to reflect the dynamics of agent communication. It also allows us to establish the important link between commitments as a deontic concept and arguments. On the one hand CTL* enables us to express all the temporal aspects related to the handling of commitments and arguments. On the other hand, dynamic logic enables us to capture the actions that agents are committed to achieve.

This paper makes a case for the importance of a formal theory of context and contextual reasoning in agent systems, and proposes a channel theoretic account for modeling the intricacies of agent reasoning in context. Using an example of reasoning about perspectives we shown that this model fulfills the formal requirements for a theory of context, and offers a nice explanatory account of contextual reasoning in terms of information flow.