The effects of public announcements, private communications, deceptive messages to groups, and so on, can all be captured by a general mechanism of updating multi-agent models with update action models, now in widespread use. There is a natural extension of the definition of a bisimulation to action models. Surely enough, updating with bisimilar action models gives the same result (modulo bisimulation). But the converse turns out to be false: update models may have the same update effects without being bisimilar. We (...) propose action emulation as a notion of equivalence more appropriate for action models, and generalizing standard bisimulation. It is proved that action emulation provides a full characterization of update effect. We first concentrate on the general case, and next focus on the important case of action models with propositional preconditions. Our notion of action emulation yields a simplification procedure for action models, and it gives designers of multi-agent systems a useful tool for comparing different ways of representing a particular communicative action. (shrink)

In this paper we present a dynamic assignment language which extends the dynamic predicate logic of Groenendijk and Stokhof [1991: 39–100] with assignment and with generalized quantifiers. The use of this dynamic assignment language for natural language analysis, along the lines of o.c. and [Barwise, 1987: 1–29], is demonstrated by examples. We show that our representation language permits us to treat a wide variety of donkey sentences: conditionals with a donkey pronoun in their consequent and quantified sentences with donkey pronouns (...) anywhere in the scope of the quantifier. It is also demonstrated that our account does not suffer from the so-called proportion problem.Discussions about the correctness or incorrectness of proposals for dynamic interpretation of language have been hampered in the past by the difficulty of seeing through the ramifications of the dynamic semantic clauses (phrased in terms of input-output behaviour) in non-trivial cases. To remedy this, we supplement the dynamic semantics of our representation language with an axiom system in the style of Hoare. While the representation languages of barwise and Groenendijk and Stokhof were not axiomatized, the rules we propose form a deduction system for the dynamic assignment language which is proved correct and complete with respect to the semantics. (shrink)

Logical frameworks for analysing the dynamics ofinformation processing abound [4, 5, 8, 10, 12, 14, 20, 22]. Some of these frameworks focus on the dynamics of the interpretation process, some on the dynamics of the process of drawing inferences, and some do both of these. Formalisms galore, so it is felt that some conceptual streamlining would pay off. This paper is part of a larger scale enterprise to pursue the obvious parallel between information processing and imperative programming. We demonstrate that (...) logical tools from theoretical computer science are relevant for the logic of information flow. More specifically, we show that the perspective of bare logic [13, 18] can fruitfully be applied to the conceptual simplification of information flow logics. Part one of this program consisted of the analysis of 'dynamic interpretation' in this way, using the example of dynamic predicate logic [10]; the results were published in [7]. The present paper constitutes the second part of the program, the analysis of 'dynamic inference'. Here we focus on Veltman’s update logic [22]. Update logic is an example of a logical framework which takes the dynamics of drawing inferences into account by modelling information growth as discarding of possibilities. This paper shows how information logics like update logic can fruitfully be studied by linking their dynamic principles to static 'correctness descriptions'. Our theme is exemplified by providing a sound and complete HoarelPratt style deduction system for update logic. The Hoare/Pratt correctness statements use modal propositional dynamic logic as assertion language and connect update logic to the modal propositional logic S5. The connection with S5 provides a clear link between the dynamic and the static semantics of update logic. The fact that update logic is decidable was noted already in [2]; the connection with S5 provides an alternative proof. The S5 connection can also be used for rephrasing the validity notions of update logic and for performing consistency checks. In conclusion, it is argued that interpreting the dynamic statements of information logics as dynamic modal operators has much wider applicability. In fact, the method can be used to axiomatize quite a wide range of information logics. (shrink)

Dynamic logic, broadly conceived, is the logic that analyses change by decomposing actions into their basic building blocks and by describing the results of performing actions in given states of the world. The actions studied by dynamic logic can be of various kinds: actions on the memory state of a computer, actions of a moving robot in a closed world, interactions between cognitive agents performing given communication protocols, actions that change the common ground between speaker and hearer in a conversation, (...) actions that change the contextually available referents in a conversation, and so on. (shrink)

Computer software is written in languages like C, Java or Haskell. In many cases social software is expressed in natural language. The paper explores connections between the areas of natural language analysis and analysis of social protocols, and proposes an extended program for natural language semantics, where the goals of natural language communication are derived from the demands of specific social protocols.