{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T07:50:59Z","timestamp":1775461859775,"version":"3.50.1"},"publisher-location":"Berlin\/Heidelberg","reference-count":25,"publisher":"Springer-Verlag","isbn-type":[{"value":"354011212X","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0025789","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T10:23:41Z","timestamp":1132395821000},"page":"311-348","source":"Crossref","is-referenced-by-count":16,"title":["Nonstandard Dynamic Logic"],"prefix":"10.1007","author":[{"given":"I.","family":"N\u00e9meti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Andr\u00e9ka,H. and N\u00e9meti,I., Completeness of Floyd's program verification method w.r.t. nonstandard time models, Seminar Notes, Math. Inst.H.A.Sci.-SZKI 1977 (in Hungarian). This was abstracted in [2]."},{"issue":"3","key":"20_CR2","first-page":"115","volume":"7","author":"H. Andr\u00e9ka","year":"1978","unstructured":"Andr\u00e9ka, H. and N\u00e9meti, I., Completeness of Floyd Logic, Bull. Section of Logic Wroclaw Vol 7, No 3, 1978, pp. 115\u2013121.","journal-title":"Bull. Section of Logic Wroclaw"},{"key":"20_CR3","first-page":"3","volume":"17","author":"H. Andr\u00e9ka","year":"1982","unstructured":"Andr\u00e9ka,H. N\u00e9meti,I. and Sain,I., A complete logic for reasoning about programs via nonstandard model theory. Part I, Part II. Theoret.Comput.Sci. 17(1982) no.2 and no.3.","journal-title":"Theoret.Comput.Sci."},{"key":"20_CR4","volume-title":"A complete first order dynamic logic. Preprint No. 810318","author":"H. Andr\u00e9ka","year":"1980","unstructured":"Andr\u00e9ka, H. N\u00e9meti, I. and Sain, I., A complete first order dynamic logic. Preprint No. 810318, Math.Inst.H.A.S., Budapest, 1980."},{"key":"20_CR5","unstructured":"Andr\u00e9ka,H. N\u00e9meti,I. and Sain,I., Henkin-type semantics for program schemes to turn negative results to positive. In: Fundamentals of Computation Theory'79 (Proc.Conf. Berlin 1979), Ed.: L. Budach, Akademie Verlag Berlin 1979. Band 2. pp. 18\u201324."},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Andr\u00e9ka, H. N\u00e9meti, I. and Sain, I., A characterization of Floyd provable programs. In: Mathematical Foundations of Computer Science'81 (Proc.Conf. Strbsk\u00e9 Pleso Czechoslovakia 1981) Lecture Notes in Computer Science, Springer Verlag, 1981.","DOI":"10.1007\/3-540-10856-4_82"},{"key":"20_CR7","unstructured":"Blok,W.J., The lattice of modal logics. J. Symbolic Logic. To appear."},{"key":"20_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-7642-0","volume-title":"Model theory for modal logic","author":"K.A. Bowen","year":"1979","unstructured":"Bowen, K.A., Model theory for modal logic. D.Reidel Publ.Co., Boston 1979, x+127 pp."},{"key":"20_CR9","volume-title":"Program proving as hand simulation with a little induction","author":"R.M. Burstall","year":"1974","unstructured":"Burstall, R.M., Program proving as hand simulation with a little induction. IFIP Congress, Stockholm, August 3\u201310, 1974."},{"key":"20_CR10","unstructured":"Chang,C.C. and Keisler,H.J., Model Theory. North-Holland, 1973."},{"key":"20_CR11","first-page":"21","volume":"14","author":"L. Csirmaz","year":"1980","unstructured":"Csirmaz, L., A survey of semantics of Floyd-Hoare derivability. CL&CL \u2014 Comput.Linguist.Comput.Lang. 14(1980)pp.21\u201342.","journal-title":"CL&CL \u2014 Comput.Linguist.Comput.Lang."},{"key":"20_CR12","unstructured":"Csirmaz,L., On the completeness of proving partial correctness. Acta Cybernet. To appear."},{"key":"20_CR13","unstructured":"Csirmaz,L. and Paris,J.B., A property of 2-sorted Peano models and program verification. Preprint Math.Inst.H.A.S. Budapest, 1981."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Gabbay,D. Pnuely,A. Shelah,S. and Stavi,J., On the temporal analysis of fairness. Preprint, Weizmann Inst. of Science, Dept. of Applied Math., May 1981.","DOI":"10.1145\/567446.567462"},{"key":"20_CR15","unstructured":"Gergely,T. and Ury,L., Time models for programs. In: Mathematical Logic in Computer Science (Proc.Coll.Salg\u00f3tarj\u00e1n 1978)Colloq.Math. Soc.J.Bolyai 26 Ed.s: Gergely,T. D\u00f6m\u00f6lki,B. North-Holland, 1981. pp.359\u2013427."},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"H\u00e1jek, P., Making dynamic logic first-order. In: Mathematical Foundations of Computer Science'81 (Proc.Conf. Strbsk\u00e9 Pleso Czechoslovakia 1981) Lecture Notes in Computer Science, Springer Verlag, 1981.","DOI":"10.1007\/3-540-10856-4_95"},{"key":"20_CR17","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/S0019-9958(75)90415-5","volume":"29","author":"D.J. Kfoury","year":"1975","unstructured":"Kfoury, D.J. and Park, D.M.R., On the termination of program schemas. Information & Control 29(1975),pp.243\u2013251.","journal-title":"Information & Control"},{"key":"20_CR18","volume-title":"Is \"Sometime\" sometimes better than \"Always\"? Intermittent assertions in proving program correctness. Preprint No. Z173","author":"Z. Manna","year":"1976","unstructured":"Manna, Z. and Waldinger, R., Is \"Sometime\" sometimes better than \"Always\"? Intermittent assertions in proving program correctness. Preprint No. Z173, Stanford Research Inst., Menlo Park, June 1976."},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Monk,J.D., Mathematical Logic. Springer Verlag, 1976.","DOI":"10.1007\/978-1-4684-9452-5"},{"key":"20_CR20","volume-title":"Nonstandard runs of Floyd provable programs","author":"I. N\u00e9meti","year":"1980","unstructured":"N\u00e9meti, I., Nonstandard runs of Floyd provable programs. Preprint, Math.Inst.H.A.S., Budapest, 1980."},{"key":"20_CR21","volume-title":"Hilbert style axiomatization of nonstandard dynamic logic","author":"I. N\u00e9meti","year":"1980","unstructured":"N\u00e9meti, I., Hilbert style axiomatization of nonstandard dynamic logic. Preprint, Math.Inst.H.A.S., Budapest, 1980."},{"key":"20_CR22","volume-title":"Results on the lattice of dynamic logics","author":"I. N\u00e9meti","year":"1981","unstructured":"N\u00e9meti, I., Results on the lattice of dynamic logics. Preprint, Math.Inst.H.A.S., Budapest, 1981."},{"key":"20_CR23","unstructured":"Richter,M.M. and Szabo,M.E., Towards a nonstandard analysis of programs. In: Proc. 2nd Victoria Symp. on Nonstandard Analysis (Victoria, British Columbia, June 1980) Lecture Notes in Mathematics, Ed.: A. Hurd, Springer Verlag, 1981."},{"key":"20_CR24","first-page":"251","volume":"13","author":"I. Sain","year":"1979","unstructured":"Sain, I., There are general rules for specifying semantics: Observations on abstract model theory. CL&CL \u2014 Comput.Linguist.Comput.Lang. 13(1979),pp.251\u2013282.","journal-title":"CL&CL \u2014 Comput.Linguist.Comput.Lang."},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Sain, I., First order dynamic logic with decidable proofs and workeable model theory. In: Fundamentals of Computation Theory'81 (Proc.Conf. Szeged 1981) Lecture Notes in Computer Science, Springer Verlag, 1981.","DOI":"10.1007\/3-540-10854-8_37"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0025789.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:55:29Z","timestamp":1607550929000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0025789"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354011212X"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0025789","relation":{},"subject":[]}}