{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:46Z","timestamp":1776316906253,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540613770","type":"print"},{"value":"9783540685074","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_33","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:36:21Z","timestamp":1330292181000},"page":"86-105","source":"Crossref","is-referenced-by-count":10,"title":["A proof system for finite trees"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Blackburn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wilfried","family":"Meyer-Viol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maarten","family":"Rijke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF01048403","volume":"4","author":"R. Backofen","year":"1995","unstructured":"Backofen, R., Rogers, J., Vijay-Shanker, K.: A first-order axiomatisation of the theory of finite trees. Journal of Logic, Language and Information, 4:5\u201339, 1995.","journal-title":"Journal of Logic, Language and Information"},{"key":"6_CR2","unstructured":"van Benthem, J., Meyer-Viol, W.: Logical Semantics of Programming. Manuscript, 1994."},{"issue":"3","key":"6_CR3","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1145\/196699.196721","volume":"1","author":"T. Berlage","year":"1994","unstructured":"Berlage, T.: A selective undo mechanism for graphical user interfaces on command objects. ACM Transactions on Computer-Human Interaction 1(3):269\u2013294, 1994.","journal-title":"ACM Transactions on Computer-Human Interaction"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Blackburn, P., Gardent, C., Meyer-Viol, W.: Talking about trees. In Proceedings of the 6th Conference of the European Chapter of the Association for Computational Linguistics, pages 21\u201329, Utrecht, The Netherlands, 1993.","DOI":"10.3115\/976744.976748"},{"key":"6_CR5","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1093\/jigpal\/2.1.3","volume":"2","author":"P. Blackburn","year":"1994","unstructured":"Blackburn, P., Meyer-Viol, W.: Linguistics, logic and finite trees. Bulletin of the IGPL 2:2\u201329, 1994.","journal-title":"Bulletin of the IGPL"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Blackburn, P., Gardent, C.: A specification language for lexical functional grammars. In Proceedings of the 7th Conference of the European Chapter of the Association for Computational Linguistics, pages 39\u201344, Dublin, Ireland, 1995.","DOI":"10.3115\/976973.976980"},{"key":"6_CR7","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(83)90059-2","volume":"25","author":"B. Courcelle","year":"1985","unstructured":"Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science 25:95\u2013169, 1985.","journal-title":"Theoretical Computer Science"},{"key":"6_CR8","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.F.: Propositional dynamic logic of regular programs. J. Comp. Syst. Sci. 18:194\u2013211, 1979.","journal-title":"J. Comp. Syst. Sci."},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Kracht, M.: Mathematical Aspects of command relations. In Proceedings of the 6th Conference of the European Chapter of the Association for Computational Linguistics, pages 240\u2013249, Utrecht, The Netherlands, 1993.","DOI":"10.3115\/976744.976773"},{"key":"6_CR10","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/BF01048404","volume":"4","author":"M. Kracht","year":"1995","unstructured":"Kracht, M.: Syntactic codes and grammar refinement. Journal of Logic, Language and Information 4:41\u201360, 1995.","journal-title":"Journal of Logic, Language and Information"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Maher, M.: Complete axiomatisations of the algebras of finite, rational and infinite trees. In Proceedings of the 3rd International Symposium on Logic in Computer Science, pages 348\u2013357, Edinburgh, Scotland, 1988.","DOI":"10.1109\/LICS.1988.5132"},{"key":"6_CR12","volume-title":"CSLI Lecture notes 7","author":"R. Goldblatt","year":"1992","unstructured":"Goldblatt, R.: Logics of Time and Computation. 2nd edition, CSLI Lecture notes 7, Center for the Study of Language and Information, Stanford, 1992.","edition":"2nd edition"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Pratt, V.: Models of program logics. In Proceedings of the 20th IEEE Symposium on Foundations of Computer Science, pages 115\u2013122, 1979.","DOI":"10.1109\/SFCS.1979.24"},{"key":"6_CR14","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141:1\u201335, 1969.","journal-title":"Transactions of the American Mathematical Society"},{"key":"6_CR15","unstructured":"Rogers, J.: A Descriptive Approach to Language-Theoretic Complexity. Studies in Logic, Language and Information, CSLI Publications, Stanford, 1996, to appear."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Smory\u0144ski, C.: Self Reference and Modal Logic. Springer Verlag, 1985.","DOI":"10.1007\/978-1-4613-8601-8"},{"key":"6_CR17","unstructured":"Spaan, E.: Complexity of Modal Logics. PhD thesis, University of Amsterdam, 1993."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:18:35Z","timestamp":1742599115000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}