{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T09:56:15Z","timestamp":1725530175343},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005954"},{"type":"electronic","value":"9783642005961"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00596-1_7","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T01:13:03Z","timestamp":1238116383000},"page":"78-91","source":"Crossref","is-referenced-by-count":1,"title":["On the Completeness of Dynamic Logic"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Leivant","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/0304-3975(82)90004-4","volume":"17","author":"H. Andreka","year":"1982","unstructured":"Andreka, H., Nemeti, I., Sain, I.: A complete logic for reasoning about programs via nonstandard model theory, Parts I and II. Theoretical Computer Science\u00a017, 193\u2013212, 259\u2013278 (1982)","journal-title":"Theoretical Computer Science"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11814771_23","volume-title":"Automated Reasoning","author":"B. Beckert","year":"2006","unstructured":"Beckert, B., Platzer, A.: Dynamic logic with non-rigid functions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol.\u00a04130, pp. 266\u2013280. Springer, Heidelberg (2006)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Blass, A., Gurevich, Y.: The underlying logic of Hoare logic. Current Trends in Theoretical Computer Science, 409\u2013436 (2001)","DOI":"10.1142\/9789812810403_0003"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E. Clarke","year":"1979","unstructured":"Clarke, E.: Programming language constructs for which it is impossible to obtain good Hoare-like axioms. J. ACM\u00a026, 129\u2013147 (1979)","journal-title":"J. ACM"},{"issue":"1","key":"7_CR5","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Computing\u00a07(1), 70\u201390 (1978)","journal-title":"SIAM J. Computing"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(81)90076-1","volume":"16","author":"L. Csirmaz","year":"1981","unstructured":"Csirmaz, L.: Programs and program verification in a general setting. Theoretical Computer Science\u00a016, 199\u2013210 (1981)","journal-title":"Theoretical Computer Science"},{"key":"7_CR7","first-page":"303","volume-title":"Intuitionism and Proof Theory","author":"S. Feferman","year":"1970","unstructured":"Feferman, S.: Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis. In: Intuitionism and Proof Theory, pp. 303\u2013326. North-Holland, Amsterdam (1970)"},{"key":"7_CR8","series-title":"LNM","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/BFb0091895","volume-title":"Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoreitc Studies","author":"S. Feferman","year":"1981","unstructured":"Feferman, S., Sieg, W.: Iterated inductive definitions and subsystems of analysis. In: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoreitc Studies. LNM, vol.\u00a0897, pp. 16\u201377. Springer, Berlin (1981)"},{"key":"7_CR9","first-page":"261","volume-title":"Proceedings of the ninth symposium on the Theory of Computing","author":"D. Harel","year":"1977","unstructured":"Harel, D., Meyer, A., Pratt, V.: Computability and completeness in logics of programs. In: Proceedings of the ninth symposium on the Theory of Computing, Providence, pp. 261\u2013268. ACM, New York (1977)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09237-4","volume-title":"First-Order Dynamic Logic","author":"D. Harel","year":"1979","unstructured":"Harel, D.: First-Order Dynamic Logic. LNCS, vol.\u00a068. Springer, Heidelberg (1979)"},{"key":"7_CR11","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-61780-9_69","volume-title":"Types for Proofs and Programs","author":"F. Honsell","year":"1996","unstructured":"Honsell, F., Miculan, M.: A natural deduction approach to dynamic logics. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 165\u2013182. Springer, Heidelberg (1996)"},{"key":"7_CR13","unstructured":"Kreisel, G.: Generalized inductive definitions. Reports for the seminar on foundations of analysis, Stanford, vol.\u00a01 \u00a73 (1963)"},{"key":"7_CR14","first-page":"95","volume-title":"Lectures on Modern Mathematics","author":"G. Kreisel","year":"1965","unstructured":"Kreisel, G.: Mathematical logic. In: Saaty, T. (ed.) Lectures on Modern Mathematics, vol.\u00a0III, pp. 95\u2013195. John Wiley, New York (1965)"},{"key":"7_CR15","first-page":"132","volume-title":"Conference Record of the Twelfth Annual Symposium on Principles of Programming Languages","author":"D. Leivant","year":"1985","unstructured":"Leivant, D.: Logical and mathematical reasoning about imperative programs. In: Conference Record of the Twelfth Annual Symposium on Principles of Programming Languages, pp. 132\u2013140. ACM, New York (1985)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-24727-2_22","volume-title":"Foundations of Software Science and Computation Structures","author":"D. Leivant","year":"2004","unstructured":"Leivant, D.: Partial correctness assertions provable in dynamic logics. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 304\u2013317. Springer, Heidelberg (2004)"},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/LICS.2006.33","volume-title":"Twenty-first Symposium on Logic in Computer Science (LiCS 2006)","author":"D. Leivant","year":"2006","unstructured":"Leivant, D.: Matching explicit and modal reasoning about programs: A proof theoretic delineation of dynamic logic. In: Twenty-first Symposium on Logic in Computer Science (LiCS 2006), Washington, pp. 157\u2013166. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Leivant, D.: Inductive completeness of logics of programs. In: Proceedings of the Workshop on Logical Frameworks and Meta-Languages (to appear, 2008)","DOI":"10.1016\/j.entcs.2008.12.119"},{"key":"7_CR19","first-page":"63","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"P. Martin-L\u00f6f","year":"1971","unstructured":"Martin-L\u00f6f, P.: Hauptsatz for the intuitionistic theory of iterated inductive definitions. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 63\u201392. North-Holland, Amsterdam (1971)"},{"key":"7_CR20","first-page":"421","volume":"19","author":"G. Mirkowska","year":"1971","unstructured":"Mirkowska, G.: On formalized systems of algorithmic logic. Bull. Acad. Polon. Sci.\u00a019, 421\u2013428 (1971)","journal-title":"Bull. Acad. Polon. Sci."},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"297","DOI":"10.2977\/prims\/1195186718","volume":"17","author":"H. Nishimura","year":"1981","unstructured":"Nishimura, H.: Arithmetical completeness in first-order dynamic logic for concurrent programs. Publ. Res. Inst. Math. Sci.\u00a017, 297\u2013309 (1981)","journal-title":"Publ. Res. Inst. Math. Sci."},{"key":"7_CR22","first-page":"109","volume-title":"Proceedings of the seventeenth symposium on Foundations of Computer Science","author":"V. Pratt","year":"1976","unstructured":"Pratt, V.: Semantical considerations on Floyd-Hoare logic. In: Proceedings of the seventeenth symposium on Foundations of Computer Science, Washington, pp. 109\u2013121. IEEE Computer Society, Los Alamitos (1976)"},{"key":"7_CR23","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1305\/ndjfl\/1093635239","volume":"30","author":"I. Sain","year":"1989","unstructured":"Sain, I.: An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic. Notre Dame Journal of Formal Logic\u00a030, 563\u2013573 (1989)","journal-title":"Notre Dame Journal of Formal Logic"},{"issue":"6","key":"7_CR24","first-page":"552","volume":"24","author":"K. Segerberg","year":"1977","unstructured":"Segerberg, K.: A completeness theorem in the modal logic of programs (preliminary report). Notics of the American Mathematical Society\u00a024(6), A\u2013552 (1977)","journal-title":"Notics of the American Mathematical Society"},{"issue":"2","key":"7_CR25","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/0304-3975(91)90336-Z","volume":"79","author":"A. Szalas","year":"1991","unstructured":"Szalas, A.: On strictly arithmetical completeness in logics of programs. Theoretical Computer Science\u00a079(2), 341\u2013355 (1991)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00596-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T16:51:48Z","timestamp":1684947108000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00596-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005954","9783642005961"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00596-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}