{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T20:10:02Z","timestamp":1746303002567,"version":"3.40.4"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319089089"},{"type":"electronic","value":"9783319089096"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08909-6_3","type":"book-chapter","created":{"date-parts":[[2014,7,11]],"date-time":"2014-07-11T06:02:05Z","timestamp":1405058525000},"page":"33-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Propositional Encoding of Constraints over Tree-Shaped Data"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Bau","sequence":"first","affiliation":[]},{"given":"Johannes","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,7,12]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and all That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, New York (1998)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Bau, A., Waldmann, J.: Propositional encoding of constraints over tree-shaped data. CoRR, abs\/1305.4957 (2013)","DOI":"10.1007\/978-3-319-08909-6_3"},{"issue":"1","key":"3_CR3","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-010-9211-0","volume":"49","author":"M Codish","year":"2012","unstructured":"Codish, M., Giesl, J., Schneider-Kamp, P., Thiemann, R.: Sat solving for termination proofs with recursive path orders and dependency pairs. J. Autom. Reasoning 49(1), 53\u201393 (2012)","journal-title":"J. Autom. Reasoning"},{"issue":"7","key":"3_CR4","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-37651-1_6","volume-title":"Programming Logics","author":"M Hanus","year":"2013","unstructured":"Hanus, M.: Functional logic programming: from theory to curry. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 123\u2013168. Springer, Heidelberg (2013)"},{"volume-title":"Haskell 98 Language and Libraries, The Revised Report","year":"2003","key":"3_CR7","unstructured":"Peyton Jones, S. (ed.): Haskell 98 Language and Libraries, The Revised Report. Cambridge University Press, Cambridge (2003)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/978-3-540-24677-0_85","volume-title":"Innovations in Applied Artificial Intelligence","author":"M Kurihara","year":"2004","unstructured":"Kurihara, M., Kondo, H.: Efficient BDD encodings for partial order constraints with application to expert systems in software verification. In: Orchard, B., Yang, C., Ali, M. (eds.) IEA\/AIE 2004. LNCS (LNAI), vol. 3029, pp. 827\u2013837. Springer, Heidelberg (2004)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Marques Silva, J.P., Sakallah, K.A.: Grasp - a new search algorithm for satisfiability. In: ICCAD, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"3_CR10","series-title":"Symbolic Computation","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"755","DOI":"10.1007\/978-3-642-11266-9_63","volume-title":"SOFSEM 2010: Theory and Practice of Computer Science","author":"H Zankl","year":"2010","unstructured":"Zankl, H., Sternagel, C., Hofbauer, D., Middeldorp, A.: Finding and certifying loops. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorn\u00fd, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol. 5901, pp. 755\u2013766. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Declarative Programming and Knowledge Management"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08909-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T19:28:51Z","timestamp":1746300531000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-08909-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089089","9783319089096"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08909-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"12 July 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}