{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:45:36Z","timestamp":1764557136439},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1988,9,1]],"date-time":"1988-09-01T00:00:00Z","timestamp":589075200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[1988,9]]},"DOI":"10.1007\/bf00370554","type":"journal-article","created":{"date-parts":[[2004,11,2]],"date-time":"2004-11-02T23:53:18Z","timestamp":1099439598000},"page":"233-241","source":"Crossref","is-referenced-by-count":56,"title":["A finite model theorem for the propositional ?-calculus"],"prefix":"10.1007","volume":"47","author":[{"given":"Dexter","family":"Kozen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"CR1","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer","year":"1979","unstructured":"M. J. Fischer and R. E. Ladner, Prepositional Dynamic Logic of regular programs, J. Comput. Syst. Sci. 18:2 (1979), pp. 194?211.","journal-title":"J. Comput. Syst. Sci."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"D. Kozen, Results on the propositional ?-calculus, in: E. Schmidt (ed.), Proc. 9th Int. Colloq. Automata, Languages, and Programming 1982, Lect. Notes in Comput. Sci. 140, Springer, 1982, pp. 348?359.","DOI":"10.1007\/BFb0012782"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"D. Kozen and R. Parikh, A decision procedure for the propositional ?-calculus, in: E. Clarke and D. Kozen (eds.), Proc. Workshop on Logics of Programs 1983, Lect. Notes in Comput. Sci. 164, Springer, 1984, pp. 313?326.","DOI":"10.1007\/3-540-12896-4_370"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S030500410005204X","volume":"79","author":"R. Laver","year":"1976","unstructured":"R. Laver, Well-quasi-ordering s and sets of finite sequences, Proc. Camb. Phil. Soc. 79 (1976), pp. 1?10.","journal-title":"Proc. Camb. Phil. Soc."},{"key":"CR5","first-page":"31","volume":"1","author":"R. Laver","year":"1978","unstructured":"R. Laver, Better-quasi-orderings and a class of trees, in: Studies in Foundations and Combinatorics, Advances in Mathematics Supplementary Studies, v.1 (1978), pp. 31?48.","journal-title":"Studies in Foundations and Combinatorics, Advances in Mathematics Supplementary Studies"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"697","DOI":"10.1017\/S0305004100039062","volume":"61","author":"C. St. J. A. Nash-Williams","year":"1965","unstructured":"C. St. J. A. Nash-Williams, On well-quasi-ordering infinite trees, Proc. Camb. Phil. Soc. 61 (1965), pp. 697?720.","journal-title":"Proc. Camb. Phil. Soc."},{"key":"CR7","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1017\/S030500410004281X","volume":"64","author":"C. St. J. A. Nash-Williams","year":"1968","unstructured":"C. St. J. A. Nash-Williams, On better-quasi-ordering transfinite sequences, Proc. Camb. Phil. Soc. 64 (1968), pp. 273?290.","journal-title":"Proc. Camb. Phil. Soc."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"V. R. Pratt, A decidable ?-calculus (preliminary report), Proc. 22nd IEEE Symp. Found. Comput. Sci., 1981, pp. 421?427.","DOI":"10.1109\/SFCS.1981.4"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"R. Streett, Propositional Dynamic Logic of looping and converse, Proc. 13th ACM Symp. Theory of Comput., 1981, pp. 375?383.","DOI":"10.1145\/800076.802492"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"R. Streett and E. A. Emerson, An elementary decision procedure for the ?-calculus, in: J. Paredaens (ed.), Proc. 11th Int. Colloq. Automata, Languages, and Programming 1984, Lect. Notes in Comput. Sci. 172, Springer, 1984, pp. 465?472.","DOI":"10.1007\/3-540-13345-3_43"},{"key":"CR11","unstructured":"D. Scott and J. de Bakker, A theory of programs, unpublished notes, Vienna, 1969."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00370554.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00370554\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00370554","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T18:24:01Z","timestamp":1585938241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00370554"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,9]]},"references-count":11,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1988,9]]}},"alternative-id":["BF00370554"],"URL":"https:\/\/doi.org\/10.1007\/bf00370554","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988,9]]}}}