Abstract
We investigate the connection between modal logic and the formal systems recently introduced for arguing about programs. The link is based on the common use of Kripke semantics. The bearing for semantics of some recent results in modal logic is explained. Finally we describe the possibilities to use intesional logic for the semantics of assignments.
Preview
Unable to display preview. Download preview PDF.
References
de Bakker, J.W. & W.P. de Roever. A calculus for recursive program schemes, in M. Nivat, (ed.) Proc. ICALP 1 (Versailles 1972), pp 167–196. North Holl. Publ. Co. 1973, Amsterdam.
de Bakker, J.W. Correctness proofs for assignment statements, Rep. IW 55/76, Mathematical Centre, 1976 Amsterdam.
Banachowski, L. e.a. An introduction to Algorithmic Logic; Mathematical investigations in the theory of programs, in A. Mazurkiewitcz & Z. Pawlak (eds.), Mathematical foundations of Computer Science, Banach Centre Publ. 1977 Warsaw.
van Benthem, J.F.A. A note on modal formulae and relational properties, J.S.L. 40 1975 pp 85–88.
Blok, W.J. The lattice of modal logics. An algebraic investigation, Rep 77-15 Dept. of Mathematics Univ. of Amsterdam 1977.
Constable, R.L. On the theory of programming logics, Proc. ACM STOC 9 1977 pp 269–285.
Donahue, J.E. Locations considered Unnecessary, Acta Informatica 8 1977 pp 221–242.
Frege, G. Uber Sinn und Bedeutung Zeitschrift für Philosophie und Philosophische Kritik (N.S.) 100 1892, pp 25–50. Transl.: On sense and Reference Translations from the writings of Gottlob Frege, P. Geach & M. Black (eds.), Basil Blackwell 1952 Oxford.
Gallin, D. Intensional and higher order Modal logic, North. Holl. Publ. Co. 1975 Amsterdam.
Goldblatt, R.I. & S.K. Thomason Axiomatic classes in propositional modal logic in J. Crossley (ed.) Algebra and logic, Proc. Autsr. Math. Summer Inst. 1974. Springer LNM 450 1975 Berlin.
Griess, D. Assignment to subscripted variables Rep TR 77-305 Dept. Comp. Sci. Cornell Univ. Ithaca NY. 1977.
Harel, D. On the correctness of Regular deterministic programs. A unifying survey, preprint MIT Dec 1977 Cambridge Mass.
Harel, D. Arithmetical completeness in logics of programs in Proc. ICALP 5 (Udine 1978), Springer LCS (to appear).
Harel, D., A. Meyer & V.R. Pratt Computability and completeness in logics of programs Proc. ACM STOC 9 1977 pp. 261–268.
Hoare, C.A.R. & N. Wirth, An axiomatic definition of the programming language PASCAL, Acta Informatica 2 1973 pp. 335–355.
Hughes, G.E. & M.J. Cresswell, An introduction to Modal logic, Methuen & Co. 1968 London.
Janssen, T.M.V. Compositionality and the form of the rules in Montague grammar Proc. 2nd Amsterdam Coll. on Montague grammar and related topics. Dept. of philosophy, Univ. of Amsterdam (to appear).
Janssen, T.M.V. & P. van Emde Boas, On the proper treatment of referencing, dereferencing and assignment in A. Salomaa & M. Steinby (eds.) Proc. ICALP 4 (Turku 1977), Springer LCS 52 pp 282–300.
Janssen, T.M.V. & P. van Emde Boas, The expressive power of intensional logic in the semantics of programming languages, in J. Gruska (ed.) Proc. MFCS 6 (Tatranska Lomnica 1977), Springer LCS 53 pp 303–311.
Kripke, S. Semantical considerations on Modal logic Acta Philosophica Fennica 16 1963 pp 83–94. Repr. in [24].
Kröger, F. LAR: A logic of Algorithmic Reasoning, Acta Informatica 8 1977 pp 243–266.
Lemmon, E.J. Algebraic semantics for modal logic I & II, J.S.L. 31 1966 pp 46–65 & 196–218.
Lewis, C.I. & C.H. Langford Symbolic logic Dover 1932 New York.
Linski, L., Reference and Modality, Oxford univ. press 1971 Oxford.
Manna, Z. & R. Waldiger Is "sometimes" sometimes better than "always", Comm. A.C.M. 21 1978 pp 159–171.
Montague, R. The proper treatment of quantification in ordinary Engish, in J. Hintikka, J. Moravcsik & P. Suppes (eds.) Approaches to natural language, Reidel 1973 Dordrecht. Repr. in R.H. Thomason (ed.) Formal Philosophy, Selected papers of Richard Montague, Yale Univ. press 1974 New Haven & London.
Pnuelli, A. The temporal logic of programs Proc. IEEE FOCS 18 1977 pp 46–57.
Pratt, V.R. Semantical considerations on Floyd-Hoare logic Proc. IEEE FOCS 17 1976 pp 109–121.
Quine, W.V. Word and Object, the MIT press 1960 Cambridge Mass.
Scott, D. & C. Strachey Towards a mathematical semantics for computer languages in J. Fox (ed.) Proc. Symp. on Computers and Automata, Polytechnic Inst. Brooklyn 1971 pp 19–46.
Strachey, C. Towards a Formal semantics in T.B. Steel (ed.) Formal language description languages for computer programming, North. Holl. Publ. Co. 1966 Amsterdam pp 198–220.
van Wijngaarden, A. e.a. (eds.) Revised report on the algorithmic language ALGOL 68 Tract MCT 50 Mathematical Centre 1976 Amsterdam.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1978 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Emde Boas, P. (1978). The connection between modal logic and algorithmic logics. In: Winkowski, J. (eds) Mathematical Foundations of Computer Science 1978. MFCS 1978. Lecture Notes in Computer Science, vol 64. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-08921-7_52
Download citation
DOI: https://doi.org/10.1007/3-540-08921-7_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-08921-6
Online ISBN: 978-3-540-35757-5
eBook Packages: Springer Book Archive