Abstract
Logical frameworks for analysing the dynamics of information 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 Hoare 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 Hoare/Pratt style deduction system for update logic. The Hoare/Pratt correctness statements use modal prepositional 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.
Similar content being viewed by others
References
J. Barwise. Noun phrases, generalized quantifiers and anaphora. In P. Gärdenfors, editor,Generalized Quantifiers: linguistic and logical approaches, pages 1–30. D. Reidel Publishing Company, Dordrecht, 1987.
J. van Benthem. Semantic parallels in natural language and computation. In H.-D. Ebbinghaus et al., editors,Logic Colloquium, Granada, 1987, pages 331–375, Amsterdam, 1989. Elsevier.
J. van Benthem. General dynamics.Theoretical Linguistics,17:159–201, 1991.
J. van Benthem.Language in Action: categories, lambdas and dynamic logic. Studies in Logic 130. Elsevier, Amsterdam, 1991.
J. van Benthem. Logic and the flow of information. Technical Report LP-91-10, ILLC, University of Amsterdam, 1991.
J. van Eijck and G. Cepparello. Dynamic modal predicate logic. Technical Report OTS-WP-CL-93-005, OTS, Utrecht, October 1993. Also in M. Kanazawa and C.J. Piñon (eds.),Dynamics, Polarity, and Quantification, CSLI, Stanford 1994.
J. van Eijck and F.J. de Vries. Dynamic interpretation and Hoare deduction.Journal of Logic, Language, and Information, 1:1–44, 1992.
P. Gärdenfors.Knowledge in Flux: Modelling the Dynamics of Epistemic States. MIT Press, 1988.
R. Goldblatt.Logics of Time and Computation, Second Edition, Revised and Expanded, volume 7 ofCSLI Lecture Notes. CSLI, Stanford, 1992 (first edition 1987). Distributed by University of Chicago Press.
J. Groenendijk and M. Stokhof. Dynamic predicate logic.Linguistics and Philosophy, 14:39–100, 1991.
J. Groenendijk and M. Stokhof. Two theories of dynamic semantics. In J. van Eijck, editor,Logics in AI-European Workshop JELIA ′90, pages 55–64, Berlin, 1991. Springer Lecture Notes in Artificial Intelligence.
I. Heim.The Semantics of Definite and Indefinite Noun Phrases. PhD thesis, University of Massachusetts, Amherst, 1982.
C.A.R. Hoare. An axiomatic basis for computer programming.Communications of the ACM, 12(10):567–580, 583, 1969.
H. Kamp. A theory of truth and semantic representation. In J. Groenendijket al., editors,Formal Methods in the Study of Language. Mathematisch Centrum, 1981.
L. Karttunen. Discourse referents. In J. McCawley, editor,Syntax and Semantics 7, pages 363–385. Academic Press, 1976.
M. Kracht. Splittings and the finite model property.Journal of Symbolic Logic, 58, 1993, pp 139–157.
D. Lewis. Score keeping in a language game.Journal of Philosophical Logic, 8:339–359, 1979.
V.Pratt. Semantical considerations on Floyd-Hoare logic.Proceedings 17th IEEE Symposium on Foundations of Computer Science, pages 109–121, 1976.
M. de Rijke. Meeting some neighbours. Technical Report LP-92-10, ILLC, University of Amsterdam, 1992. Also in Van Eijck and Visser (eds.),Logic and Information Flow, MIT Press, 1994.
M. de Rijke. A system of dynamic modal logic. Technical Report LP-92-08, ILLC, University of Amsterdam, 1992.
R. Stalnaker. Pragmatics. In D. Davidson and G. Harman, editors,Semantics of Natural Language, pages 380–397. Reidel, 1972.
F. Veltman. Defaults in update semantics. Technical report, Department of Philosophy, University of Amsterdam, 1991. To appear in the Journal of Philosophical Logic.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
van Eijck, J., de Vries, FJ. Reasoning about update logic. J Philos Logic 24, 19–45 (1995). https://doi.org/10.1007/BF01052729
Issue Date:
DOI: https://doi.org/10.1007/BF01052729