{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:38:28Z","timestamp":1725521908892},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787686"},{"type":"electronic","value":"9783540787693"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-78769-3_1","type":"book-chapter","created":{"date-parts":[[2008,11,26]],"date-time":"2008-11-26T12:05:56Z","timestamp":1227701156000},"page":"1-7","source":"Crossref","is-referenced-by-count":1,"title":["Proving Termination with (Boolean) Satisfaction"],"prefix":"10.1007","author":[{"given":"Michael","family":"Codish","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1-2","key":"1_CR1","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(1-2), 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/11693024_16","volume-title":"Programming Languages and Systems","author":"M. Codish","year":"2006","unstructured":"Codish, M., Lagoon, V., Schachte, P., Stuckey, P.J.: Size-Change Termination Analysis in k-Bits. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 230\u2013245. Springer, Heidelberg (2006)"},{"key":"1_CR3","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":"P.J. Stuckey","year":"2006","unstructured":"Stuckey, P.J., Codish, M., Lagoon, V.: Solving Partial Order Constraints for LPO Termination. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 4\u201318. Springer, Heidelberg (2006)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Codish, M., Lagoon, V., Stuckey, P.J.: Logic programming with satisfiability. The Journal of Theory and Practice of Logic Programming\u00a08(1) (2008), \n                    \n                       http:\/\/arxiv.org\/pdf\/cs.PL\/0702072","DOI":"10.1017\/S1471068407003146"},{"key":"1_CR5","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., Schneider-Kamp, P., Lagoon, V., Thiemann, R., Giesl, J.: SAT Solving for Argument Filterings. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 30\u201344. Springer, Heidelberg (2006)"},{"issue":"7","key":"1_CR6","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\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"1_CR7","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. Theoretical Computer Science\u00a017, 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"issue":"1\/2","key":"1_CR8","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation\u00a03(1\/2), 69\u2013116 (1987)","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR9","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. Waldmann","year":"2006","unstructured":"Waldmann, J., Zantema, H., Endrullis, J.: 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":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"key":"1_CR11","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. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated Termination Proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 210\u2013220. Springer, Heidelberg (2004)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-32033-3_14","volume-title":"Term Rewriting and Applications","author":"A. Middeldorp","year":"2005","unstructured":"Middeldorp, A., Hirokawa, N.: Tyrolean Termination Tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 175\u2013184. Springer, Heidelberg (2005)"},{"key":"1_CR14","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":"J. Waldmann","year":"2006","unstructured":"Waldmann, J., Hofbauer, D.: Termination of String Rewriting with Matrix Interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 328\u2013342. Springer, Heidelberg (2006)"},{"key":"1_CR15","unstructured":"Kamin, S., Levy, J.-J.: Two generalizations of the recursive path ordering. In: Department of Computer Science, University of Illinois, Urbana, IL (viewed December 2005) (1980), \n                    \n                      http:\/\/www.ens-lyon.fr\/LIP\/REWRITING\/OLD_PUBLICATIONS_ON_TERMINATION"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","volume":"40","author":"M. Krishnamoorthy","year":"1985","unstructured":"Krishnamoorthy, M., Narendran, P.: On recursive path ordering. Theoretical Computer Science\u00a040, 323\u2013328 (1985)","journal-title":"Theoretical Computer Science"},{"key":"1_CR17","series-title":"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.\u00a03029, pp. 827\u2013837. Springer, Heidelberg (2004)"},{"issue":"3","key":"1_CR18","first-page":"81","volume":"36","author":"C.S. Lee","year":"2001","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. ACM SIGPLAN Notices, Proceedings of POPL 2001\u00a036(3), 81\u201392 (2001)","journal-title":"ACM SIGPLAN Notices, Proceedings of POPL 2001"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-73449-9_23","volume-title":"Term Rewriting and Applications","author":"C. March\u00e9","year":"2007","unstructured":"March\u00e9, C., Zantema, H.: The Termination Competition. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 303\u2013313. Springer, Heidelberg (2007) (To appear)"},{"key":"1_CR20","unstructured":"MiniSAT solver (viewed December 2005), \n                    \n                      http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\n                    \n                    \n                  ."},{"key":"1_CR21","unstructured":"SAT4J satisfiability library for Java, \n                    \n                      http:\/\/www.sat4j.org"},{"key":"1_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-540-74621-8_18","volume-title":"Frontiers of Combining Systems","author":"P. Schneider-Kamp","year":"2007","unstructured":"Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving Termination Using Recursive Path Orders and SAT Solving. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 267\u2013282. Springer, Heidelberg (2007)"},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-27813-9_12","volume-title":"Computer Aided Verification","author":"M. Talupur","year":"2004","unstructured":"Talupur, M., Sinha, N., Strichman, O., Pnueli, A.: Range allocation for separation logic. In: Alur, R., Peled, D.A. (eds.) CAV 2004, vol.\u00a03114, pp. 148\u2013161. Springer, Heidelberg (2004)"},{"key":"1_CR24","unstructured":"The termination problem data base, \n                    \n                      http:\/\/www.lri.fr\/~marche\/tpdb\/"},{"key":"1_CR25","unstructured":"Wielemaker, J.: An overview of the SWI-Prolog programming environment. In: Mesnard, F., Serebenik, A. (eds.) Proceedings of the 13th International Workshop on Logic Programming Environments, Katholieke Universiteit Leuven. CW 371, (December 2003) pp. 1\u201316. (2003)"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-540-73449-9_29","volume-title":"Term Rewriting and Applications","author":"H. Zankl","year":"2007","unstructured":"Zankl, H., Middeldorp, A.: Satisfying KBO constraints. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 389\u2013403. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78769-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,4]],"date-time":"2019-03-04T04:58:48Z","timestamp":1551675528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78769-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540787686","9783540787693"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78769-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}