{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:04:22Z","timestamp":1765667062209},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642408847"},{"type":"electronic","value":"9783642408854"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40885-4_24","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T07:20:19Z","timestamp":1378884019000},"page":"343-358","source":"Crossref","is-referenced-by-count":26,"title":["Term Rewriting with Logical Constraints"],"prefix":"10.1007","author":[{"given":"Cynthia","family":"Kop","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Nishida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Community. SMT-LIB, http:\/\/www.smtlib.org\/"},{"issue":"3","key":"24_CR2","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term rewriting systems. Theor. Comput. Sci.\u00a017(3), 279\u2013301 (1982)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-02959-2_22","volume-title":"Automated Deduction \u2013 CADE-22","author":"S. Falke","year":"2009","unstructured":"Falke, S., Kapur, D.: A term rewriting approach to the automated termination analysis of imperative programs. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 277\u2013293. Springer, Heidelberg (2009)"},{"key":"24_CR4","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-31365-3_20","volume-title":"Automated Reasoning","author":"S. Falke","year":"2012","unstructured":"Falke, S., Kapur, D.: Rewriting induction + linear arithmetic = decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol.\u00a07364, pp. 241\u2013255. Springer, Heidelberg (2012)"},{"key":"24_CR5","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Schmidt-Schau\u00df, M. (ed.) Proc. RTA 2011. LIPIcs, vol.\u00a010, pp. 41\u201350. Dagstuhl (2011)"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-27705-4_21","volume-title":"Verified Software: Theories, Tools, Experiments","author":"S. Falke","year":"2012","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of imperative programs using bitvector arithmetic. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 261\u2013277. Springer, Heidelberg (2012)"},{"issue":"2","key":"24_CR7","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10817-010-9215-9","volume":"47","author":"C. Fuhs","year":"2011","unstructured":"Fuhs, C., Giesl, J., Parting, M., Schneider-Kamp, P., Swiderski, S.: Proving Termination by Dependency Pairs and Inductive Theorem Proving. Journal of Automated Reasoning\u00a047(2), 133\u2013160 (2011)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02348-4_3","volume-title":"Rewriting Techniques and Applications","author":"C. Fuhs","year":"2009","unstructured":"Fuhs, C., Giesl, J., Pl\u00fccker, M., Schneider-Kamp, P., Falke, S.: Proving termination of integer term rewriting. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 32\u201347. Springer, Heidelberg (2009)"},{"issue":"2","key":"24_CR9","first-page":"100","volume":"1","author":"Y. Furuichi","year":"2008","unstructured":"Furuichi, Y., Nishida, N., Sakai, M., Kusakari, K., Sakabe, T.: Approach to procedural-program verification based on implicit induction of constrained term rewriting systems. IPSJ Trans. Program.\u00a01(2), 100\u2013121 (2008)","journal-title":"IPSJ Trans. Program."},{"issue":"2","key":"24_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1890028.1890030","volume":"33","author":"J. Giesl","year":"2011","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems\u00a033(2), 7:1\u20137:39 (2011)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"24_CR11","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Fran\u00e7aise d\u2019Intelligence Artificielle\u00a04(3), 9\u201352 (1990)","journal-title":"Revue Fran\u00e7aise d\u2019Intelligence Artificielle"},{"issue":"1","key":"24_CR12","first-page":"173","volume":"28","author":"N. Nakabayashi","year":"2010","unstructured":"Nakabayashi, N., Nishida, N., Kusakari, K., Sakabe, T., Sakai, M.: Lemma generation method in rewriting induction for constrained term rewriting systems. Computer Software\u00a028(1), 173\u2013189 (2010) (in Japanese)","journal-title":"Computer Software"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of java bytecode by term rewriting. In: Lynch, C. (ed.) Proc. RTA 2010. LIPIcs, vol.\u00a06, pp. 259\u2013276. Dagstuhl (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-642-22531-4_9","volume-title":"Functional and Constraint Logic Programming","author":"T. Sakata","year":"2011","unstructured":"Sakata, T., Nishida, N., Sakabe, T.: On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs. In: Kuchen, H. (ed.) WFLP 2011. LNCS, vol.\u00a06816, pp. 138\u2013155. Springer, Heidelberg (2011)"},{"issue":"4-6","key":"24_CR15","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1017\/S1471068410000165","volume":"10","author":"P. Schneider-Kamp","year":"2010","unstructured":"Schneider-Kamp, P., Giesl, J., Str\u00f6der, T., Serebrenik, A., Thiemann, R.: Automated termination analysis for logic programs with cut. Theory and Practice of Logic Programming\u00a010(4-6), 365\u2013381 (2010)","journal-title":"Theory and Practice of Logic Programming"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40885-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,5]],"date-time":"2022-03-05T19:52:15Z","timestamp":1646509935000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40885-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642408847","9783642408854"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40885-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}