{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:00:19Z","timestamp":1777125619380,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540727873","type":"print"},{"value":"9783540727880","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72788-0_33","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T12:25:22Z","timestamp":1183033522000},"page":"340-354","source":"Crossref","is-referenced-by-count":65,"title":["SAT Solving for Termination Analysis with Polynomial Interpretations"],"prefix":"10.1007","author":[{"given":"Carsten","family":"Fuhs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Zankl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","unstructured":"Annov, E., et al.: A SAT-based implementation for RPO termination. In: Short Papers of LPAR\u00a0\u201906 (2006)"},{"key":"33_CR2","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"33_CR3","unstructured":"Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical Report AIB-2001-09, RWTH Aachen (2001)"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/11805618_2","volume-title":"Term Rewriting and Applications","author":"M. Codish","year":"2006","unstructured":"Codish, M., Lagoon, V., Stuckey, P.: Solving partial order constraints for LPO termination. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 4\u201318. Springer, Heidelberg (2006)"},{"key":"33_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/11916277_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Codish","year":"2006","unstructured":"Codish, M., et al.: SAT solving for argument filterings. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 30\u201344. Springer, Heidelberg (2006)"},{"key":"33_CR7","unstructured":"Contejean, E., et al.: CiME, http:\/\/cime.lri.fr"},{"issue":"4","key":"33_CR8","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10817-005-9022-x","volume":"34","author":"E. Contejean","year":"2005","unstructured":"Contejean, E., et al.: Mechanically proving termination using polynomial interpretations. J. Aut. Reason.\u00a034(4), 325\u2013363 (2005)","journal-title":"J. Aut. Reason."},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"33_CR10","unstructured":"Empirical evaluation of \u201cSAT solving for termination analysis with polynomial interpretations\u201d, http:\/\/aprove.informatik.rwth-aachen.de\/eval\/SATPOLO"},{"key":"33_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/11814771_47","volume-title":"Automated Reasoning","author":"J. Endrullis","year":"2006","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 574\u2013588. Springer, Heidelberg (2006)"},{"key":"33_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The DP framework: Combining Techniques for Automated Termination Proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/11805618_23","volume-title":"Term Rewriting and Applications","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., et al.: Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 297\u2013312. Springer, Heidelberg (2006)"},{"key":"33_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the DP framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"3","key":"33_CR15","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., et al.: Mechanizing and improv- ing dependency pairs. Journal of Automated Reasoning\u00a037(3), 155\u2013203 (2006)","journal-title":"Journal of Automated Reasoning"},{"issue":"1-2","key":"33_CR16","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/j.ic.2004.10.004","volume":"199","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation\u00a0199(1-2), 172\u2013199 (2005)","journal-title":"Information and Computation"},{"issue":"4","key":"33_CR17","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1016\/j.ic.2006.08.010","volume":"205","author":"N. Hirokawa","year":"2007","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. Information and Computation\u00a0205(4), 474\u2013511 (2007)","journal-title":"Information and Computation"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/11805618_25","volume-title":"Term Rewriting and Applications","author":"D. Hofbauer","year":"2006","unstructured":"Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 328\u2013342. Springer, Heidelberg (2006)"},{"issue":"1","key":"33_CR19","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1005983105493","volume":"21","author":"H. Hong","year":"1998","unstructured":"Hong, H., Jaku\u0161, D.: Testing positiveness of polynomials. JAR\u00a021(1), 23\u201338 (1998)","journal-title":"JAR"},{"key":"33_CR20","unstructured":"Lankford, D.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)"},{"key":"33_CR21","unstructured":"Le Berre, D., et al.: SAT4J satisfiability library for Java, http:\/\/www.sat4j.org"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","first-page":"177","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J. Giesl","year":"2007","unstructured":"Giesl, J., et al.: Automated Termination Analysis for Logic Programs by Term Rewriting. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol.\u00a04407, pp. 177\u2013193. Springer, Heidelberg (2007)"},{"key":"33_CR23","doi-asserted-by":"crossref","first-page":"61","DOI":"10.3233\/SAT190020","volume":"2","author":"H.M. Sheini","year":"2006","unstructured":"Sheini, H.M., Sakallah, K.A.: Pueblo: A hybrid pseudo-boolean SAT solver. Journal on Satisfiability, Boolean Modeling and Computation\u00a02, 61\u201396 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"33_CR24","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"33_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-540-69507-3_50","volume-title":"SOFSEM 2007: Theory and Practice of Computer Science","author":"H. Zankl","year":"2007","unstructured":"Zankl, H., Hirokawa, N., Middeldorp, A.: Constraints for argument filterings. In: van Leeuwen, J., et al. (eds.) SOFSEM 2007. LNCS, vol.\u00a04362, pp. 579\u2013590. Springer, Heidelberg (2007)"},{"key":"33_CR26","unstructured":"Zankl, H., Middeldorp, A.: KBO as a satisfaction problem. In: Proc. WST\u201906 (2006)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72788-0_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:05:11Z","timestamp":1605762311000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72788-0_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727873","9783540727880"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72788-0_33","relation":{},"subject":[]}}