{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:43Z","timestamp":1740099043897,"version":"3.37.3"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319735788"},{"type":"electronic","value":"9783319735795"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-73579-5_10","type":"book-chapter","created":{"date-parts":[[2018,1,2]],"date-time":"2018-01-02T02:32:44Z","timestamp":1514860364000},"page":"153-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Dynamic Logic: A Personal Perspective"],"prefix":"10.1007","author":[{"given":"Vaughan","family":"Pratt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,1,3]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Barr, M.: $$*$$ \u2217 -Autonomous Categories. Lecture Notes in Mathematics, vol. 752. Springer, Berlin (1979)","DOI":"10.1007\/BFb0064579"},{"key":"10_CR2","volume-title":"The Foundations of Mathematics","author":"EW Beth","year":"1959","unstructured":"Beth, E.W.: The Foundations of Mathematics. North Holland, Amsterdam (1959)"},{"key":"10_CR3","unstructured":"Brock, J.D., Ackerman, W.B.: An anomaly in the specifications of nondeterministic packet systems. Technical report Computation Structures Group Note CSG-33, MIT Lab. for Computer Science, November 1977"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Cannon, J.J.: A general purpose group theory program. In: Proceedings of the Second International Conference Theory of Groups, Canberra, pp. 204\u2013217 (1973)","DOI":"10.1007\/978-3-662-21571-5_17"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Cannon, J.J.: A draft description of the group theory language cayley. In: Proceedings of the Third ACM Symposium on Symbolic and Algebraic Computation, SYMSAC 1976, pp. 66\u201384. ACM, New York (1976)","DOI":"10.1145\/800205.806325"},{"key":"10_CR6","unstructured":"de Bakker, J.W., de Roever, W.P.: A calculus for recursive program schemes. In: Nivat, M. (ed.) Automata, Languages and Programming, pp. 167\u2013196. North Holland (1972)"},{"key":"10_CR7","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"issue":"2","key":"10_CR8","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1016\/S0022-0000(76)80034-7","volume":"12","author":"A Ehrenfeucht","year":"1976","unstructured":"Ehrenfeucht, A., Zeiger, P.: Complexity measures for regular expressions. J. Comput. Syst. Sci. 12(2), 134\u2013146 (1976)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. In: Proceedings of the 9th ACM Symposium on Theory of Computing, pp. 194\u2013211, Boulder, May 1977. Journal version: Propositional dynamic logic of regular programs, JCSS 18:2 (1979)","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"10_CR11","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G Gentzen","year":"1934","unstructured":"Gentzen, G.: Investigations into logical deductions. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1934)"},{"issue":"5","key":"10_CR12","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1016\/S0019-9958(67)91165-5","volume":"10","author":"EM Gold","year":"1967","unstructured":"Gold, E.M.: Language identification in the limit. Inf. Control 10(5), 447\u2013474 (1967)","journal-title":"Inf. Control"},{"issue":"2","key":"10_CR13","doi-asserted-by":"crossref","first-page":"427","DOI":"10.3233\/FI-1981-4210","volume":"IV","author":"J Grabowski","year":"1981","unstructured":"Grabowski, J.: On partial languages. Fundam. Inform. IV(2), 427\u2013498 (1981)","journal-title":"Fundam. Inform."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D., Meyer, A.R., Pratt, V.R.: Computability and completeness in logics of programs. In: Proceedings of the 9th Annual ACM Symposium on Theory of Computation, pp. 261\u2013268 (1977)","DOI":"10.1145\/800105.803416"},{"issue":"8","key":"10_CR15","doi-asserted-by":"crossref","first-page":"597","DOI":"10.2307\/2321009","volume":"84","author":"L Henkin","year":"1977","unstructured":"Henkin, L.: The logic of equality. Amer. Math. Mon. 84(8), 597\u2013612 (1977)","journal-title":"Amer. Math. Mon."},{"key":"10_CR16","first-page":"7","volume":"8","author":"KJJ Hintikka","year":"1955","unstructured":"Hintikka, K.J.J.: Form and content ni quantification theory. Acta Philos. Fenni. 8, 7\u201355 (1955)","journal-title":"Acta Philos. Fenni."},{"key":"10_CR17","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"10_CR18","first-page":"135","volume":"3","author":"CAR Hoare","year":"1974","unstructured":"Hoare, C.A.R., Lauer, P.E.: Consistent and complementary formal theories of the semantics of programming languages. Acta Inform. 3, 135\u2013153 (1974)","journal-title":"Acta Inform."},{"key":"10_CR19","doi-asserted-by":"crossref","first-page":"891","DOI":"10.2307\/2372123","volume":"73","author":"B J\u00f3nsson","year":"1951","unstructured":"J\u00f3nsson, B., Tarski, A.: Boolean algebras with operators. Part I. Amer. J. Math. 73, 891\u2013939 (1951)","journal-title":"Part I. Amer. J. Math."},{"issue":"2","key":"10_CR20","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1137\/0206024","volume":"6","author":"DE Knuth","year":"1977","unstructured":"Knuth, D.E., Morris, J., Pratt, V.R.: Fast pattern matching in strings. SIAM J. Comput. 6(2), 323\u2013350 (1977)","journal-title":"SIAM J. Comput."},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A representation theorem for models of $$*$$ \u2217 -free PDL. Technical report RC7864, IBM, September 1979","DOI":"10.1007\/3-540-10003-2_83"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 23 (1983)","DOI":"10.7146\/dpb.v11i146.7420"},{"issue":"1","key":"10_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S Kripke","year":"1959","unstructured":"Kripke, S.: A completeness theorem in modal logic. J. Symb. Logic 24(1), 1\u201314 (1959)","journal-title":"J. Symb. Logic"},{"key":"10_CR24","first-page":"83","volume":"16","author":"S Kripke","year":"1963","unstructured":"Kripke, S.: Semantical considerations on modal logic. Acta Philos. Fenn. 16, 83\u201394 (1963)","journal-title":"Acta Philos. Fenn."},{"issue":"3","key":"10_CR25","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"RE Ladner","year":"1977","unstructured":"Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6(3), 467\u2013480 (1977)","journal-title":"SIAM J. Comput."},{"key":"10_CR26","unstructured":"Litvintchouk, S.D., Pratt, V.R.: A proof checker for dynamic logic. In: 5th International Joint Conference on A.I., pp. 552\u2013558, August 1977"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Technical report DAIMI Report PB-78, Aarhus University, Aarhus (1977)","DOI":"10.7146\/dpb.v6i78.7691"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Nelson, G., Oppen, D.C.: Fast decision algorithms based on union and find. In: 18th IEEE Symposium on Foundations of Computer Science, October 1977","DOI":"10.1109\/SFCS.1977.12"},{"key":"10_CR29","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0304-3975(82)90030-5","volume":"17","author":"I N\u00e9meti","year":"1982","unstructured":"N\u00e9meti, I.: Every free algebra in the variety generated by the representable dynamic algebras is separable and representable. Theoret. Comput. Sci. 17, 343\u2013347 (1982)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR30","series-title":"LNCS","first-page":"403","volume-title":"MFCS 1978","author":"R Parikh","year":"1978","unstructured":"Parikh, R.: A completeness result for a propositional dynamic logic. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol. 64, pp. 403\u2013415. Springer, Heidelberg (1978)"},{"key":"10_CR31","unstructured":"Petri, C.A.: Fundamentals of a theory of asynchronous information flow. In: Proceedings of the IFIP Congress 62, Munich, pp. 386\u2013390 (1962). North-Holland, Amsterdam"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201357, October 1977","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR33","unstructured":"Pratt, V.R.: Translation of lewis carroll\u2019s syllogisms into logic. Masters Thesis, August 1969"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Proceedings of the 17th Annual IEEE Symposium on Foundations of Computer Science, pp. 109\u2013121, October 1976","DOI":"10.1109\/SFCS.1976.27"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: A practical decision method for propositional dynamic logic. In: Proceedings of the 10th Annual ACM Symposium on Theory of Computing, San Diego, pp. 326\u2013337, May 1978","DOI":"10.1145\/800133.804362"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Axioms or algorithms. In: Proceedings of the 6th Symposium on Mathematical Foundations of Computer Science, Olomouc, Czech. (1979)","DOI":"10.1007\/3-540-09526-8_12"},{"key":"10_CR37","unstructured":"Pratt, V.R.: Dynamic algebras: Examples, constructions, applications. Technical report MIT\/LCS\/TM-138, M.I.T. Laboratory for Computer Science, July 1979"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Dynamic logic. In: Proceedings of the 6th Conference on Logic, Methodology, and Philosophy of Science, Hanover, West Germany, pp. 251\u2013261 (1979)","DOI":"10.1016\/S0049-237X(09)70196-X"},{"key":"10_CR39","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Process logic. In: Proceedings of the 6th Annual ACM Symposium on Principles of Programming Languages, San Antonio, pp. 93\u2013100, January 1979","DOI":"10.1145\/567752.567761"},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Dynamic algebras and the nature of induction. In: 12th ACM Symposium on Theory of Computation, Los Angeles, April 1980","DOI":"10.1145\/800141.804649"},{"key":"10_CR41","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","volume":"2","author":"VR Pratt","year":"1980","unstructured":"Pratt, V.R.: A near optimal method for reasoning about action. J. Comput. Syst. Sci. 2, 231\u2013254 (1980). Also MIT\/LCS\/TM-113, M.I.T., Sept. 1978","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR42","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: A decidable mu-calculus. In: Proceedings of the 22nd IEEE Conference on Foundations of Computer Science, pp. 421\u2013427, October 1981","DOI":"10.1109\/SFCS.1981.4"},{"key":"10_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/BFb0025792","volume-title":"Logics of Programs","author":"VR Pratt","year":"1982","unstructured":"Pratt, V.R.: Using graphs to understand PDL. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 387\u2013396. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025792"},{"key":"10_CR44","unstructured":"Pratt, V.R.: Position statement. Circulated at the Panel on Mathematics of Parallel Processes, chair A.R.G. Milner, IFIP-83, September 1983"},{"key":"10_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-15670-4_9","volume-title":"Seminar on Concurrency","author":"V Pratt","year":"1985","unstructured":"Pratt, V.: The pomset model of parallel processes: unifying the temporal and the spatial. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 180\u2013196. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15670-4_9"},{"key":"10_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-16047-7_39","volume-title":"The Analysis of Concurrent Systems","author":"V Pratt","year":"1985","unstructured":"Pratt, V.: Two-way channel with disconnect. In: Denvir, B.T., Harwood, W.T., Jackson, M.I., Wray, M.J. (eds.) The Analysis of Concurrent Systems. LNCS, vol. 207, pp. 110\u2013114. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-16047-7_39"},{"key":"10_CR47","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Modeling concurrency with geometry. In: Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages, pp. 311\u2013322, January 1991","DOI":"10.1145\/99583.99625"},{"key":"10_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BFb0084795","volume-title":"CONCUR \u201992","author":"VR Pratt","year":"1992","unstructured":"Pratt, V.R.: The duality of time and information. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 237\u2013253. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0084795"},{"issue":"3\/4","key":"10_CR49","first-page":"571","volume":"50","author":"VR Pratt","year":"1992","unstructured":"Pratt, V.R.: Dynamic algebras: examples, constructions, applications. Stud. Logica 50(3\/4), 571\u2013605 (1992)","journal-title":"Stud. Logica"},{"issue":"4","key":"10_CR50","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1017\/S0960129503004031","volume":"13","author":"VR Pratt","year":"2003","unstructured":"Pratt, V.R.: Transition and cancellation in concurrency and branching time. Math. Struct. Comp. Sci. 13(4), 485\u2013529 (2003). Special issue on the difference between sequentiality and concurrency","journal-title":"Math. Struct. Comp. Sci."},{"key":"10_CR51","unstructured":"Rasiowa, H., Sikorski, R.: The Mathematics of Metamathematics. Polska Akademia Nauk. Monografie matematyczne, vol. 41. Drukarnia Uniwersytetu, Warsaw (1963)"},{"key":"10_CR52","doi-asserted-by":"crossref","unstructured":"Rennie, M.K.: Models for multiply modal systems. Zeitschr. j. math. Logik und Grundlagen d. Math. 16, 175\u2013186 (1970)","DOI":"10.1002\/malq.19700160207"},{"key":"10_CR53","unstructured":"Salwicki, A.: Formalized algorithmic languages. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. 18(5), 227\u2013232 (1970)"},{"key":"10_CR54","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"WJ Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 177\u2013192 (1970)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR55","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R Smullyan","year":"1968","unstructured":"Smullyan, R.: First Order Logic. Springer, Berlin (1968)"},{"key":"10_CR56","first-page":"37","volume":"40","author":"M Stone","year":"1936","unstructured":"Stone, M.: The theory of representations for Boolean algebras. Trans. Amer. Math. Soc. 40, 37\u2013111 (1936)","journal-title":"Trans. Amer. Math. Soc."},{"key":"10_CR57","doi-asserted-by":"crossref","unstructured":"Valiev, M.K.: On axiomatization of deterministic propositional dynamic logic. In: Proceedings of the 6th Symposium on Mathematical Foundations of Computer Science, Olomouc, Czech. (1979)","DOI":"10.1007\/3-540-09526-8_48"},{"key":"10_CR58","first-page":"9","volume":"43","author":"II Zhegalkin","year":"1927","unstructured":"Zhegalkin, I.I.: On the technique of calculating propositions in symbolic logic. Matematicheskii Sbornik 43, 9\u201328 (1927)","journal-title":"Matematicheskii Sbornik"}],"container-title":["Lecture Notes in Computer Science","Dynamic Logic. New Trends and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73579-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,11]],"date-time":"2022-08-11T17:15:09Z","timestamp":1660238109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73579-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319735788","9783319735795"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73579-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}