{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,21]],"date-time":"2023-01-21T01:27:01Z","timestamp":1674264421289},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,12,15]],"date-time":"2010-12-15T00:00:00Z","timestamp":1292371200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,6]]},"DOI":"10.1007\/s10817-010-9211-0","type":"journal-article","created":{"date-parts":[[2010,12,15]],"date-time":"2010-12-15T19:00:14Z","timestamp":1292439614000},"page":"53-93","source":"Crossref","is-referenced-by-count":13,"title":["SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs"],"prefix":"10.1007","volume":"49","author":[{"given":"Michael","family":"Codish","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","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"}]}],"member":"297","published-online":{"date-parts":[[2010,12,15]]},"reference":[{"issue":"1\u20132","key":"9211_CR1","doi-asserted-by":"crossref","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. Theor. Comp. Sci. 236(1\u20132), 133\u2013178 (2000)","journal-title":"Theor. Comp. Sci."},{"key":"9211_CR2","unstructured":"Audemard, G., Simon, L.: glucose. http:\/\/www.lri.fr\/~simon\/glucose\/"},{"key":"9211_CR3","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, Cambridge (1998)"},{"key":"9211_CR4","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Codish, M.: A SAT-based approach to size change termination with global ranking functions. In: TACAS \u201908. LNCS 4963, pp. 218\u2013232 (2007)","DOI":"10.1007\/978-3-540-78800-3_16"},{"issue":"2","key":"9211_CR5","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A Ben Cherifa","year":"1987","unstructured":"Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program. 9(2), 137\u2013159 (1987)","journal-title":"Sci. Comput. Program"},{"key":"9211_CR6","unstructured":"Biere, A.: PrecoSAT. http:\/\/fmv.jku.at\/precosat\/"},{"key":"9211_CR7","doi-asserted-by":"crossref","unstructured":"Bofill, M., Busquets, D., Villaret, M.: A declarative approach to robust weighted max-SAT. In: PPDP \u201910, pp. 67\u201376. ACM (2010)","DOI":"10.1145\/1836089.1836098"},{"key":"9211_CR8","doi-asserted-by":"crossref","unstructured":"Borralleras, C., Lucas, S., Navarro-Marset, R., Rodr\u00edguez-Carbonell, E., Rubio, A.: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. In: CADE\u00a0\u201909. LNAI 5663, pp. 294\u2013305 (2009)","DOI":"10.1007\/978-3-642-02959-2_23"},{"key":"9211_CR9","doi-asserted-by":"crossref","unstructured":"Codish, M., Schneider-Kamp, P., Lagoon, V., Thiemann, R., Giesl, J.: SAT solving for argument filterings. In: LPAR \u201906. LNAI 4246, pp. 30\u201344 (2006)","DOI":"10.1007\/11916277_3"},{"key":"9211_CR10","doi-asserted-by":"crossref","first-page":"193","DOI":"10.3233\/SAT190056","volume":"5","author":"M Codish","year":"2008","unstructured":"Codish, M., Lagoon, V., Stuckey, P.J.: Solving partial order constraints for LPO termination. Journal on Satisfiability, Boolean Modeling and Computation 5, 193\u2013215 (2008)","journal-title":"Boolean Modeling and Computation"},{"key":"9211_CR11","doi-asserted-by":"crossref","unstructured":"Codish, M., Genaim, S., Stuckey, P.J.: A declarative encoding of telecommunications feature subscription in SAT. In: PPDP \u201909, pp. 255\u2013266. ACM (2009)","DOI":"10.1145\/1599410.1599442"},{"key":"9211_CR12","doi-asserted-by":"crossref","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. Comp. Sci. 17, 279\u2013301 (1982)","journal-title":"Theor. Comp. Sci."},{"key":"9211_CR13","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSAT. http:\/\/minisat.se\/"},{"issue":"1\u20134","key":"9211_CR14","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satifiability, Boolean Modeling and Computation 2(1\u20134), 1\u201326 (2006)","journal-title":"Journal on Satifiability, Boolean Modeling and Computation"},{"issue":"2\u20133","key":"9211_CR15","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2\u20133), 195\u2013220 (2008)","journal-title":"J. Autom. Reason."},{"key":"9211_CR16","doi-asserted-by":"crossref","unstructured":"Feydy, T., Schutt, A., Stuckey, P.J.: Global difference constraint propagation for finite domain solvers. In: PPDP\u00a0\u201908, pp. 226\u2013235. ACM (2008)","DOI":"10.1145\/1389449.1389478"},{"key":"9211_CR17","doi-asserted-by":"crossref","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: SAT\u00a0\u201907. LNCS 4501, pp. 340\u2013354 (2007)","DOI":"10.1007\/978-3-540-72788-0_33"},{"key":"9211_CR18","doi-asserted-by":"crossref","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: RTA \u201908. LNCS 5117, pp. 110\u2013125 (2008)","DOI":"10.1007\/978-3-540-70590-1_8"},{"key":"9211_CR19","doi-asserted-by":"crossref","unstructured":"Fuhs, C., Navarro-Marset, R., Otto, C., Giesl, J., Lucas, S., Schneider-Kamp, P.: Search techniques for rational polynomial orders. In: AISC \u201908. LNAI 5144, pp. 109\u2013124 (2008)","DOI":"10.1007\/978-3-540-85110-3_10"},{"key":"9211_CR20","unstructured":"Geser, A.: Relative Termination. PhD Thesis, University of Passau, Germany (1990)"},{"key":"9211_CR21","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: FroCoS \u201905. LNAI 3717, pp. 216\u2013231 (2005)","DOI":"10.1007\/11559306_12"},{"key":"9211_CR22","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: LPAR \u201904. LNAI 3452, pp. 301\u2013331 (2005)","DOI":"10.1007\/978-3-540-32275-7_21"},{"key":"9211_CR23","doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: IJCAR \u201906. LNAI 4130, pp. 281\u2013286 (2006)","DOI":"10.1007\/11814771_24"},{"issue":"3","key":"9211_CR24","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155\u2013203 (2006)","journal-title":"J. Autom. Reason"},{"key":"9211_CR25","unstructured":"Gotlieb, A.: TCAS software verification using constraint programming. Knowl. Eng. Rev. (2010, to appear)"},{"issue":"1\u20132","key":"9211_CR26","doi-asserted-by":"crossref","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. Inf. Comput. 199(1\u20132), 172\u2013199 (2005)","journal-title":"Inf. Comput."},{"issue":"4","key":"9211_CR27","doi-asserted-by":"crossref","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. Inf. Comput. 205(4), 474\u2013511 (2007)","journal-title":"Inf. Comput."},{"key":"9211_CR28","doi-asserted-by":"crossref","first-page":"1407","DOI":"10.1016\/j.artint.2010.07.001","volume":"174","author":"C Jefferson","year":"2010","unstructured":"Jefferson, C., Moore, N.C.A., Nightingale, P., Petrie, K.E.: Implementing logical connectives in constraint programming. Artif. Intell. 174, 1407\u20131429 (2010)","journal-title":"Artif. Intell"},{"key":"9211_CR29","unstructured":"Kamin, S., L\u00e9vy, J.J.: Two Generalizations of the Recursive Path Ordering. Technical Report, University of Illinois, IL, USA (1980)"},{"key":"9211_CR30","doi-asserted-by":"crossref","unstructured":"Koprowski, A., Middeldorp, A.: Predictive labeling with dependency pairs using SAT. In: CADE \u201907. LNAI 4603, pp. 410\u2013425 (2007)","DOI":"10.1007\/978-3-540-73595-3_31"},{"key":"9211_CR31","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","volume":"40","author":"MS Krishnamoorthy","year":"1985","unstructured":"Krishnamoorthy, M.S., Narendran, P.: On recursive path ordering. Theor. Comp. Sci. 40, 323\u2013328 (1985)","journal-title":"Theor. Comp. Sci."},{"key":"9211_CR32","doi-asserted-by":"crossref","unstructured":"Kurihara, M., Kondo, H.: Efficient BDD encodings for partial order constraints with application to expert systems in software verification. In: IEA\/AIE \u201904. LNCS 3029, pp. 827\u2013837 (2004)","DOI":"10.1007\/978-3-540-24677-0_85"},{"key":"9211_CR33","doi-asserted-by":"crossref","unstructured":"Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: PPDP \u201999. LNCS 1702, pp. 47\u201361 (1999)","DOI":"10.1007\/10704567_3"},{"key":"9211_CR34","unstructured":"Lankford, D.: On Proving Term Rewriting Systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)"},{"key":"9211_CR35","unstructured":"Le Berre, D., Parrain, A.: SAT4J. http:\/\/www.sat4j.org"},{"key":"9211_CR36","doi-asserted-by":"crossref","unstructured":"Lescanne, P.: Computer experiments with the REVE term rewriting system generator. In: POPL \u201983, pp. 99\u2013108. ACM (1983)","DOI":"10.1145\/567067.567078"},{"key":"9211_CR37","doi-asserted-by":"crossref","unstructured":"Lescuyer, S., Conchon, S.: Improving Coq propositional reasoning using a lazy CNF conversion scheme. In: FroCoS \u201909. LNCS 5749, pp. 287\u2013303 (2009)","DOI":"10.1007\/978-3-642-04222-5_18"},{"key":"9211_CR38","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. In: 3rd Hawaii International Conference on System Science, pp. 789\u2013792 (1970)"},{"key":"9211_CR39","doi-asserted-by":"crossref","unstructured":"Mari\u00ebn, M., Wittocx, J., Denecker, M., Bruynooghe, M.: SAT(ID): Satisfiability of propositional logic extended with inductive definitions. In: SAT \u201908. LNCS 4996, pp. 211\u2013224 (2008)","DOI":"10.1007\/978-3-540-79719-7_20"},{"key":"9211_CR40","doi-asserted-by":"crossref","unstructured":"Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and SAT solving. In: FroCoS \u201907. LNAI 4720, pp. 267\u2013282 (2007)","DOI":"10.1007\/978-3-540-74621-8_18"},{"issue":"2","key":"9211_CR41","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/s10601-008-9061-0","volume":"14","author":"N Tamura","year":"2009","unstructured":"Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints 14(2), 254\u2013272 (2009)","journal-title":"Constraints"},{"key":"9211_CR42","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. Reprinted in J. Siekmann and G. Wrightson (eds.), Automation of Reasoning, 2:466-483 (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"9211_CR43","doi-asserted-by":"crossref","unstructured":"Zankl, H., Hirokawa, N., Middeldorp, A.: Constraints for argument filterings. In: SOFSEM \u201907. LNCS 4362, pp. 579\u2013590 (2007)","DOI":"10.1007\/978-3-540-69507-3_50"},{"issue":"2","key":"9211_CR44","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-009-9131-z","volume":"43","author":"H Zankl","year":"2009","unstructured":"Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. J. Autom. Reason. 43(2), 173\u2013201 (2009)","journal-title":"J. Autom. Reason"},{"issue":"1","key":"9211_CR45","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/s10472-009-9144-7","volume":"56","author":"H Zankl","year":"2009","unstructured":"Zankl, H., Middeldorp, A.: Increasing interpretations. Ann. Math. Artif. Intell. 56(1), 87\u2013108 (2009)","journal-title":"Ann. Math. Artif. Intell."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9211-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9211-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9211-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,14]],"date-time":"2020-06-14T18:26:47Z","timestamp":1592159207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9211-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,15]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["9211"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9211-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12,15]]}}}