{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:05:37Z","timestamp":1762459537472,"version":"3.41.0"},"reference-count":123,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T00:00:00Z","timestamp":1499817600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"crossref","award":["TIN2015-69175-C4-1-R"],"award-info":[{"award-number":["TIN2015-69175-C4-1-R"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003359","name":"Generalitat Valenciana","doi-asserted-by":"crossref","award":["PROMETEOII\/2015\/013"],"award-info":[{"award-number":["PROMETEOII\/2015\/013"]}],"id":[{"id":"10.13039\/501100003359","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"publisher","award":["JCI-2012-13528"],"award-info":[{"award-number":["JCI-2012-13528"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,4]]},"DOI":"10.1007\/s10817-017-9419-3","type":"journal-article","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T20:47:05Z","timestamp":1499892425000},"page":"465-501","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9923-2108","authenticated-orcid":false,"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ra\u00fal","family":"Guti\u00e9rrez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,12]]},"reference":[{"key":"9419_CR1","doi-asserted-by":"crossref","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST\u201910. LNCS, vol. 6486, pp. 201\u2013208 (2011)","DOI":"10.1007\/978-3-642-17796-5_12"},{"key":"9419_CR2","unstructured":"Alarc\u00f3n, B., Lucas, S., Navarro-Marset, R.: Using matrix interpretations over the reals in proofs of termination. In: Proceedings of PROLE\u201909, pp. 255\u2013264 (2009)"},{"key":"9419_CR3","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., Guti\u00e9rrez, R.: A Transformational Approach to Resource Analysis with Typed-Norms. Revised Selected Papers from LOPSTR\u201913. LNCS, vol. 8901, pp 38\u201353 (2013)","DOI":"10.1007\/978-3-319-14125-1_3"},{"issue":"4\u20135","key":"9419_CR4","doi-asserted-by":"crossref","first-page":"635","DOI":"10.1017\/S1471068415000289","volume":"15","author":"E Angelis de","year":"2015","unstructured":"de Angelis, E., Fioravante, F., Pettorossi, A., Proietti, M.: Proving correctness of imperative programs by linearizing constrained Horn clauses. Theory Pract. Log. Program. 15(4\u20135), 635\u2013650 (2015)","journal-title":"Theory Pract. Log. Program."},{"key":"9419_CR5","doi-asserted-by":"crossref","unstructured":"de Angelis, E., Fioravante, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions by program specialization. In: Proceedings of PPDP\u201915, pp. 91\u2013102. ACM Press, New York (2015)","DOI":"10.1145\/2790449.2790529"},{"issue":"11","key":"9419_CR6","first-page":"1","volume":"2001","author":"T Aoto","year":"2001","unstructured":"Aoto, T.: Solution to the problem of zantema on a persistent property of term rewriting systems. J. Funct. Log. Program. 2001(11), 1\u201320 (2001)","journal-title":"J. Funct. Log. Program."},{"key":"9419_CR7","volume-title":"Handbook of Mathematical Logic","author":"J Barwise","year":"1977","unstructured":"Barwise, J.: An Introduction to First-Order Logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic. North-Holland, Amsterdam (1977)"},{"key":"9419_CR8","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0003-4843(74)90016-3","volume":"7","author":"J Barwise","year":"1974","unstructured":"Barwise, J.: Axioms for Abstract Model Theory. Ann. Math. Log. 7, 221\u2013265 (1974)","journal-title":"Ann. Math. Log."},{"key":"9419_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03718-8","volume-title":"Real Algebraic Geometry","author":"J Bochnak","year":"1998","unstructured":"Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry. Springer, Berlin (1998)"},{"key":"9419_CR10","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/S0021-9800(70)80014-X","volume":"8","author":"G Birkhoff","year":"1970","unstructured":"Birkhoff, G., Lipson, J.D.: Heterogeneous algebras. J. Comb. Theory 8, 115\u2013133 (1970)","journal-title":"J. Comb. Theory"},{"key":"9419_CR11","doi-asserted-by":"crossref","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The Barcelogic SMT Solver. In: Proceedings of CAV\u201908. LNCS, vol. 5123, pp. 294\u2013298 (2008)","DOI":"10.1007\/978-3-540-70545-1_27"},{"key":"9419_CR12","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn-clause solvers for program verification. In: Fields of Logic and Computation II\u2014Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. LNCS, vol. 9300, pp. 24\u201351 (2015)","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"9419_CR13","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn-clauses. In: Proceedings of SAS\u201913. LNCS vol. 7935, pp. 105\u2013125 (2013)","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"9419_CR14","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: Proceedings of SMT\u201912, EPiC Series in Computing, vol. 20, pp. 3\u201311 (2013)","DOI":"10.29007\/1l7f"},{"key":"9419_CR15","unstructured":"Bliss, G.A.: Algebraic Functions. Dover (2004)"},{"key":"9419_CR16","doi-asserted-by":"crossref","unstructured":"Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: On Lexicographic Termination Ordering With Space Bound Certifications. Revised Papers from PSI 2001. LNCS, vol. 2244, pp. 482\u2013493 (2001)","DOI":"10.1007\/3-540-45575-2_46"},{"key":"9419_CR17","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139164931","volume-title":"Computability and Logic","author":"GS Boolos","year":"2002","unstructured":"Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002)","edition":"4"},{"key":"9419_CR18","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/s10817-010-9196-8","volume":"48","author":"C Borralleras","year":"2012","unstructured":"Borralleras, C., Lucas, S., Oliveras, A., Rodr\u00edguez, E., Rubio, A.: SAT modulo linear arithmetic for solving polynomial constraints. J. Autom. Reason. 48, 107\u2013131 (2012)","journal-title":"J. Autom. Reason."},{"key":"9419_CR19","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BF02127744","volume":"18","author":"H-J B\u00fcrckert","year":"1996","unstructured":"B\u00fcrckert, H.-J., Hollunder, B., Laux, A.: On Skolemization in constrained logics. Ann. Math. Artif. Intell. 18, 95\u2013131 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9419_CR20","unstructured":"Burstall, R.M., Goguen, J.A.: Putting Theories together to make specifications. In: Proceedings of IJCAI\u201977, pp. 1045\u20131058. William Kaufmann (1977)"},{"key":"9419_CR21","doi-asserted-by":"crossref","unstructured":"Caplain, M.: Finding invariant assertions for proving programs. In: Proceedings of the International Conference on Reliable Software, pp. 165\u2013171. ACM Press, New York (1975)","DOI":"10.1145\/800027.808436"},{"key":"9419_CR22","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"CL Chang","year":"1973","unstructured":"Chang, C.L., Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Orlando (1973)"},{"key":"9419_CR23","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude\u2014A High-Performance Logical Framework. LNCS 4350, (2007)"},{"key":"9419_CR24","unstructured":"Cohn, A.G.: Improving the expressiveness of many sorted logic. In: Proceedings of the National Conference on Artificial Intelligence, pp. 84\u201387. AAAI Press, Menlo Park (1983)"},{"issue":"4","key":"9419_CR25","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s10817-005-9022-x","volume":"34","author":"E Contejean","year":"2006","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325\u2013363 (2006)","journal-title":"J. Autom. Reason."},{"key":"9419_CR26","first-page":"43","volume":"6","author":"DC Cooper","year":"1971","unstructured":"Cooper, D.C.: Programs for mechanical program verification. Mach. Intell. 6, 43\u201359 (1971). Edinburgh University Press","journal-title":"Mach. Intell."},{"key":"9419_CR27","first-page":"91","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91\u201399 (1972)","journal-title":"Mach. Intell."},{"key":"9419_CR28","doi-asserted-by":"crossref","unstructured":"Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretations. In: Proceedings of SOFSEM\u201910. LNCS, vol. 5901, pp. 283\u2013295 (2010)","DOI":"10.1007\/978-3-642-11266-9_24"},{"key":"9419_CR29","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: Logical abstract domains and interpretations. In: The Future of Sofware Engineering, pp. 48\u201371. Springer, New York (2011)","DOI":"10.1007\/978-3-642-15187-3_3"},{"key":"9419_CR30","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic Discovery of linear restraints among variables of a program. In: Conference Record of POPL\u201978, pp. 84\u201396. ACM Press, New York (1978)","DOI":"10.1145\/512760.512770"},{"key":"9419_CR31","volume-title":"Introduction to Lattices and Order","author":"BA Davey","year":"1990","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"issue":"2","key":"9419_CR32","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/356599.356602","volume":"4","author":"B Elspas","year":"1972","unstructured":"Elspas, B., Levitt, K.N., Waldinger, R.J., Waksman, A.: An assessment of techniques for proving program correctness. Comput. Surv. 4(2), 97\u2013147 (1972)","journal-title":"Comput. Surv."},{"issue":"4","key":"9419_CR33","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/321978.321991","volume":"23","author":"MH Emdem van","year":"1976","unstructured":"van Emdem, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23(4), 733\u2013742 (1976)","journal-title":"J. ACM"},{"key":"9419_CR34","doi-asserted-by":"crossref","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Proceedings of IJCAR\u201906. LNCS, vol. 4130, pp. 574\u2013588 (2006)","DOI":"10.1007\/11814771_47"},{"issue":"2\u20133","key":"9419_CR35","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":"9419_CR36","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19\u201332 (1967)","journal-title":"Math. Asp. Comput. Sci."},{"key":"9419_CR37","doi-asserted-by":"crossref","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Proceedings of RTA\u201908. LNCS, vol. 5117, pp. 110\u2013125 (2008)","DOI":"10.1007\/978-3-540-70590-1_8"},{"key":"9419_CR38","doi-asserted-by":"crossref","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. J. Autom. Reason. 47, 133\u2013160 (2011)","journal-title":"J. Autom. Reason."},{"key":"9419_CR39","unstructured":"Fuhs, C., Kop, C.: Polynomial interpretations for higher-order rewriting. In: Proceedings of RTA\u201912. LIPIcs, vol. 15, pp. 176\u2013192 (2012)"},{"key":"9419_CR40","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, AMAST Series, (1998)","DOI":"10.1142\/3831"},{"key":"9419_CR41","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1016\/j.scico.2015.05.004","volume":"111","author":"M Gaboardi","year":"2015","unstructured":"Gaboardi, M., P\u00e9choux, R.: On bounding space usage of streams using interpretation analysis. Sci. Comput. Program. 111, 395\u2013425 (2015)","journal-title":"Sci. Comput. Program."},{"key":"9419_CR42","doi-asserted-by":"crossref","unstructured":"Giesl, J., Mesnard, F., Rubio, A., Thiemann, R., Waldmann, J.: Termination competition (termCOMP 2015). In: Proceedings of CADE\u201915. LNCS, vol. 9195, pp. 105\u2013108 (2015)","DOI":"10.1007\/978-3-319-21401-6_6"},{"key":"9419_CR43","doi-asserted-by":"crossref","unstructured":"Giesl, J., Str\u00f6der, T., Schneider-Kamp, P., Emmes, F., Fuhs, C.: Symbolic evaluation graphs and term rewriting\u2014a general methodology for analyzing logic programs. In: Proceedings of the PPDP\u201912, pp. 1\u201312. ACM Press (2012)","DOI":"10.1145\/2370776.2370778"},{"key":"9419_CR44","doi-asserted-by":"crossref","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7 (2011)","DOI":"10.1145\/1890028.1890030"},{"key":"9419_CR45","doi-asserted-by":"crossref","unstructured":"Gnaedig, I.: Termination of Order-sorted Rewriting. In: Proceedings of ALP\u201992. LNCS, vol. 632, pp. 37\u201352 (1992)","DOI":"10.1007\/BFb0013818"},{"key":"9419_CR46","unstructured":"Goguen, J.A.: Order-Sorted Algebra. Semantics and Theory of Computation Report 14, UCLA (1978)"},{"key":"9419_CR47","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0304-3975(84)90134-8","volume":"31","author":"JA Goguen","year":"1984","unstructured":"Goguen, J.A., Burstall, R.M.: Some fundamental algebraic tools for the semantics of computation. Part 1: comma categories, colimits, signatures and theories. Theoret. Comput. Sci. 31, 175\u2013209 (1984)","journal-title":"Theoret. Comput. Sci."},{"key":"9419_CR48","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0304-3975(84)90036-7","volume":"31","author":"JA Goguen","year":"1984","unstructured":"Goguen, J.A., Burstall, R.M.: Some fundamental algebraic tools for the semantics of computation. Part 2 signed and abstract theories. Theoret. Comput. Sci. 31, 263\u2013295 (1984)","journal-title":"Theoret. Comput. Sci."},{"key":"9419_CR49","doi-asserted-by":"crossref","unstructured":"Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT\u201987. LNCS, vol. 250, pp. 1\u201322 (1987)","DOI":"10.1007\/BFb0014969"},{"key":"9419_CR50","unstructured":"Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current Trends in Programming Methodology, pp. 80\u2013149. Prentice Hall (1978)"},{"issue":"4","key":"9419_CR51","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1145\/24714.24719","volume":"22","author":"JA Goguen","year":"1987","unstructured":"Goguen, J.A., Meseguer, J.: Remarks on remarks on many-sorted equational logic. Sigplan Notices 22(4), 41\u201348 (1987)","journal-title":"Sigplan Notices"},{"key":"9419_CR52","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"9419_CR53","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-6541-0","volume-title":"Software Engineering with OBJ: Algebraic Specification in Action","author":"JA Goguen","year":"2000","unstructured":"Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, Boston (2000)"},{"key":"9419_CR54","doi-asserted-by":"crossref","unstructured":"Grebenshikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of PLDI\u201912, pp. 405\u2013416. ACM Press (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"9419_CR55","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining Abstract Interpreters. In: Proceedings of PLDI\u201906, pp. 376\u2013386. ACM Press (2006)","DOI":"10.1145\/1133981.1134026"},{"key":"9419_CR56","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Proceedings of CAV\u201915, Part I. LNCS, vol. 9206, pp. 343\u2013361 (2015)","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"9419_CR57","unstructured":"Guti\u00e9rrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories. In: Proceedings of PROLE\u201916, pp. 215\u2013230 (2016). http:\/\/zenon.dsic.upv.es\/ages\/"},{"issue":"3","key":"9419_CR58","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1145\/356674.356677","volume":"8","author":"SL Hantler","year":"1976","unstructured":"Hantler, S.L., King, J.C.: An introduction to proving the correctness of programs. ACM Comput. Surv. 8(3), 331\u2013353 (1976)","journal-title":"ACM Comput. Surv."},{"key":"9419_CR59","first-page":"495","volume":"6","author":"P Hayes","year":"1971","unstructured":"Hayes, P.: A logic of actions. Mach. Intell. 6, 495\u2013520 (1971). Edinburgh University Press, Edinburgh","journal-title":"Mach. Intell."},{"key":"9419_CR60","doi-asserted-by":"crossref","unstructured":"Heidergott, B., Olsder, G.J., van der Woude, J.: Max plus at work. A course on max-plus algebra and its applications. In: Modeling and Analysis of Synchronized Systems, Princeton University Press (2006)","DOI":"10.1515\/9781400865239"},{"key":"9419_CR61","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Proceedings of IJCAR 2008. LNCS, vol. 5195, pp. 364\u2013379 (2008)","DOI":"10.1007\/978-3-540-71070-7_32"},{"issue":"10","key":"9419_CR62","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013583 (1969)","journal-title":"Commun. ACM"},{"key":"9419_CR63","doi-asserted-by":"crossref","unstructured":"Hodges, W.: Elementary Predicate Logic. Handbook of Philosophical Logic, vol. 1, pp. 1\u2013131. Reidel Publishing Company (1983)","DOI":"10.1007\/978-94-009-7066-3_1"},{"key":"9419_CR64","volume-title":"A Shorter Model Theory","author":"W Hodges","year":"1997","unstructured":"Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997)"},{"key":"9419_CR65","doi-asserted-by":"crossref","unstructured":"Hofbauer, D.: Termination proofs by context-dependent interpretation. In: Proceedings of RTA\u201901. LNCS, vol. 2051, pp. 108\u2013121 (2001)","DOI":"10.1007\/3-540-45127-7_10"},{"key":"9419_CR66","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s002000100062","volume":"12","author":"D Hofbauer","year":"2001","unstructured":"Hofbauer, D.: Termination proofs for ground rewrite systems. interpretations and derivational complexity. Appl. Algebra Eng. Commun. Comput. 12, 21\u201338 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9419_CR67","doi-asserted-by":"crossref","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Proceedings of RTA\u201989. LNCS, vol. 355, pp. 167\u2013177 (1989)","DOI":"10.1007\/3-540-51081-8_107"},{"key":"9419_CR68","doi-asserted-by":"crossref","unstructured":"Hull, T.E., Enright, W.H., Sedgwick, A.E.: The correctness of numerical algorithms. In: Proceedings of PAAP\u201972, pp. 66\u201373 (1972)","DOI":"10.1145\/800235.807073"},{"key":"9419_CR69","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S Igarashi","year":"1975","unstructured":"Igarashi, S., London, R.L., Luckham, D.: Automatic program verification I: a logical basis and its implementation. Acta Inform. 4, 145\u2013182 (1975)","journal-title":"Acta Inform."},{"key":"9419_CR70","unstructured":"Iwami, M.: Persistence of termination of term rewriting systems with ordered sorts. In: Proceedings of 5th JSSST Workshop on Programming and Programming Languages, Shizuoka, Japan, pp. 47\u201356. (2003)"},{"key":"9419_CR71","unstructured":"Iwami, M.: Persistence of termination for non-overlapping term rewriting systems. In: Proceedings of Algebraic Systems, Formal Languages and Conventional and Unconventional Computation Theory, Kokyuroku RIMS, University of Kyoto, vol. 1366, pp. 91\u201399 (2004)"},{"issue":"4","key":"9419_CR72","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S Katz","year":"1976","unstructured":"Katz, S., Manna, Z.: Logical analysis of programs. Commun. ACM 19(4), 188\u2013206 (1976)","journal-title":"Commun. ACM"},{"issue":"2","key":"9419_CR73","doi-asserted-by":"crossref","first-page":"98","DOI":"10.2307\/2269080","volume":"4","author":"CH Langford","year":"1939","unstructured":"Langford, C.H.: Review: \u00dcber deduktive Theorien mit mehreren Sorten von Grunddingen. J. Symb. Log. 4(2), 98 (1939)","journal-title":"J. Symb. Log."},{"key":"9419_CR74","unstructured":"Lankford, D.S.: Some approaches to equality for computational logic: a survey and assessment. Memo ATP-36, Automatic Theorem Proving Project, University of Texas, Austin, TX"},{"key":"9419_CR75","doi-asserted-by":"crossref","unstructured":"London, R.L.: The current state of proving programs correct. In: Proceedings of ACM\u201972, vol. 1, pp. 39\u201346. ACM (1972)","DOI":"10.1145\/800193.805820"},{"issue":"3","key":"9419_CR76","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1051\/ita:2005029","volume":"39","author":"S Lucas","year":"2005","unstructured":"Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theor. Inform. Appl. 39(3), 547\u2013586 (2005)","journal-title":"RAIRO Theor. Inform. Appl."},{"key":"9419_CR77","doi-asserted-by":"crossref","first-page":"32","DOI":"10.4204\/EPTCS.200.3","volume":"200","author":"S Lucas","year":"2015","unstructured":"Lucas, S.: Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving. Electron. Proc. Theor. Comput. Sci. 200, 32\u201347 (2015)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"9419_CR78","doi-asserted-by":"crossref","unstructured":"Lucas, S.: Use of logical models for proving operational termination in general logics. In: Selected Papers from WRLA\u201916. LNCS, vol. 9942, pp. 1\u201321 (2016)","DOI":"10.1007\/978-3-319-44802-2_2"},{"key":"9419_CR79","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1016\/j.ipl.2005.05.002","volume":"95","author":"S Lucas","year":"2005","unstructured":"Lucas, S., March\u00e9, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inform. Proces. Lett. 95, 446\u2013453 (2005)","journal-title":"Inform. Proces. Lett."},{"key":"9419_CR80","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Proceedings of AISC\u201914. LNAI, vol. 8884, pp. 7\u201318 (2014)","DOI":"10.1007\/978-3-319-13770-4_3"},{"key":"9419_CR81","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Proceedings of PPDP\u201908 , pp. 108\u2013119. ACM Press (2008)","DOI":"10.1145\/1389449.1389463"},{"key":"9419_CR82","doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J.: Proving operational termination of declarative programs in general logics. In: Proceedings of PPDP\u201914, pp. 111\u2013122. ACM Digital Library (2014)","DOI":"10.1145\/2643135.2643152"},{"key":"9419_CR83","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1016\/j.jlamp.2016.03.003","volume":"86","author":"S Lucas","year":"2017","unstructured":"Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236\u2013268 (2017)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"9419_CR84","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/S0022-0000(69)80009-7","volume":"3","author":"Z Manna","year":"1969","unstructured":"Manna, Z.: The correctness of programs. J. Comput. Syst. Sci. 3, 119\u2013127 (1969)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"9419_CR85","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/321510.321516","volume":"16","author":"Z Manna","year":"1969","unstructured":"Manna, Z.: Properties of programs and the first-order predicate calculus. J. ACM 16(2), 244\u2013255 (1969)","journal-title":"J. ACM"},{"key":"9419_CR86","doi-asserted-by":"crossref","unstructured":"Manna, Z.: Termination of programs represented as interpreted graphs. In: Proceedings of AFIPS\u201970, pp. 83\u201389 (1970)","DOI":"10.1145\/1476936.1476956"},{"key":"9419_CR87","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science, pp. 789\u2013792 (1970)"},{"issue":"3","key":"9419_CR88","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/321592.321606","volume":"17","author":"Z Manna","year":"1970","unstructured":"Manna, Z., Pnueli, A.: Formalization of properties of functional programs. J. ACM 17(3), 555\u2013569 (1970)","journal-title":"J. ACM"},{"issue":"4","key":"9419_CR89","first-page":"27","volume":"10","author":"Y-I Marion","year":"2009","unstructured":"Marion, Y.-I., P\u00e9choux, R.: Sup-interpretations, a semantic method for static analysis of program resources. ACM Trans. Comput. Log. 10(4), 27 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"9419_CR90","doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Palomino, M.: Theoroidal maps as algebraic simulations. Revised Selected Papers from WADT\u201904. LNCS, vol. 3423, pp. 126\u2013143 (2005)","DOI":"10.1007\/978-3-540-31959-7_8"},{"issue":"4","key":"9419_CR91","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine. Part I. Commun. ACM 3(4), 184\u2013195 (1960)","journal-title":"Commun. ACM"},{"key":"9419_CR92","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: General logics. In: Ebbinghaus, H.D., et al. (eds.) Logic Colloquium\u201987, pp. 275\u2013329. North-Holland (1989)","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"9419_CR93","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Revised Selected Papers from LOPSTR\u201915. LNCS, vol. 9527, pp. 36\u201353 (2015)","DOI":"10.1007\/978-3-319-27436-2_3"},{"key":"9419_CR94","doi-asserted-by":"crossref","unstructured":"Middeldorp, A.: Matrix interpretations for polynomial derivational complexity of rewrite systems. In: Proceedings of LPAR\u201912. LNCS, vol. 7180, p. 12 (2012)","DOI":"10.1007\/978-3-642-28717-6_2"},{"key":"9419_CR95","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0043-0","volume-title":"Understanding Formal Methods","author":"J-F Monin","year":"2003","unstructured":"Monin, J.-F.: Understanding Formal Methods. Springer, London (2003)"},{"key":"9419_CR96","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1016\/j.scico.2014.04.006","volume":"111","author":"M Montenegro","year":"2015","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: Space consumption analysis by abstract interpretation: inference of recursive functions. Sci. Comput. Program. 111, 426\u2013457 (2015)","journal-title":"Sci. Comput. Program."},{"issue":"9","key":"9419_CR97","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L Moura de","year":"2011","unstructured":"de Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"9419_CR98","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/BF01966091","volume":"6","author":"P Naur","year":"1966","unstructured":"Naur, P.: Proof of algorithms by general snapshots. Bit 6, 310\u2013316 (1966)","journal-title":"Bit"},{"key":"9419_CR99","unstructured":"Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. In: Proceedings of RTA\u201911. LIPICS, vol. 10, pp. 251\u2013266 (2011)"},{"key":"9419_CR100","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002)"},{"key":"9419_CR101","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Lysne, O.: Order-sorted termination: the unsorted way. In: Proceedings of ALP\u201996. LNCS, vol. 1139, pp. 92\u2013106 (1996)","DOI":"10.1007\/3-540-61735-3_6"},{"key":"9419_CR102","doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of java bytecode by term rewriting. In: Proceedings of RTA\u201910. LIPICS, vol. 6, pp. 259\u2013276 (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"9419_CR103","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1016\/j.tcs.2012.11.003","volume":"467","author":"R P\u00e9choux","year":"2013","unstructured":"P\u00e9choux, R.: Synthesis of sup-interpretations: a survey. Theoret. Comput. Sci. 467, 30\u201352 (2013)","journal-title":"Theoret. Comput. Sci."},{"key":"9419_CR104","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: IEEE Computer Society Proceedings of LICS\u201904, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"9419_CR105","volume-title":"Positive Polynomials. From Hilbert\u2019s 17th Problem to Real Algebra","author":"A Prestel","year":"2001","unstructured":"Prestel, A., Delzell, C.N.: Positive Polynomials. From Hilbert\u2019s 17th Problem to Real Algebra. Springer, Berlin (2001)"},{"key":"9419_CR106","doi-asserted-by":"crossref","DOI":"10.1142\/6237","volume-title":"A Course in Linear Algebra with Applications","author":"DJS Robinson","year":"2006","unstructured":"Robinson, D.J.S.: A Course in Linear Algebra with Applications, 2nd edn. World Scientific Publishing, Co, Singapore (2006)","edition":"2"},{"key":"9419_CR107","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Proceedings of CAV\u201913, vol. 8044, pp. 347\u2013363 (2013)","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"9419_CR108","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Amsterdam (1986)"},{"issue":"4","key":"9419_CR109","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/BF01448954","volume":"115","author":"A Schmidt","year":"1938","unstructured":"Schmidt, A.: \u00dcber deduktive Theorien mit mehreren Sorten von Grunddingen. Matematische Annalen 115(4), 485\u2013506 (1938)","journal-title":"Matematische Annalen"},{"key":"9419_CR110","doi-asserted-by":"crossref","unstructured":"Schmidt-Schauss, M.: Computational Aspects Of An Order-Sorted Logic With Term Declarations. PhD Thesis, Fachbereich Informatik der Universit\u00e4t Kaiserslautern (1988)","DOI":"10.1007\/BFb0024065"},{"key":"9419_CR111","volume-title":"Foundations without Foundationalism: A Case for Second-Order Logic","author":"S Shapiro","year":"1991","unstructured":"Shapiro, S.: Foundations without Foundationalism: A Case for Second-Order Logic. Clarendon Press, New York (1991)"},{"issue":"2","key":"9419_CR112","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"RE Shostak","year":"1979","unstructured":"Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351\u2013360 (1979)","journal-title":"J. ACM"},{"key":"9419_CR113","doi-asserted-by":"crossref","DOI":"10.1515\/9781400882007","volume-title":"Theory of Formal Systems","author":"RM Smullyan","year":"1961","unstructured":"Smullyan, R.M.: Theory of Formal Systems. Princeton University Press, Princeton (1961)"},{"key":"9419_CR114","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)","edition":"2"},{"key":"9419_CR115","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y Toyama","year":"1987","unstructured":"Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inform. Process. Lett. 25, 141\u2013143 (1987)","journal-title":"Inform. Process. Lett."},{"key":"9419_CR116","unstructured":"Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, University Mathematics Laboratory, Cambridge, pp. 67\u201369 (1949)"},{"key":"9419_CR117","doi-asserted-by":"crossref","unstructured":"Urban, C.: The abstract domain of segmented ranking functions. In: Proceeding of SAS\u201913. LNCS, vol. 7935, pp. 43\u201362 (2013)","DOI":"10.1007\/978-3-642-38856-9_5"},{"key":"9419_CR118","doi-asserted-by":"crossref","unstructured":"Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Proceedings of TACAS\u201916. LNCS, vol. 9636, pp. 54\u201370 (2016)","DOI":"10.1007\/978-3-662-49674-9_4"},{"key":"9419_CR119","unstructured":"Waldmann, J.: Matrix interpretations on polyhedral domains. In: Proceedings of RTA\u201915. LIPICS, vol. 26, pp. 318\u2013333 (2015)"},{"key":"9419_CR120","unstructured":"Waldmann, J., Bau, A., Noeth, E.: Matchbox termination prover. http:\/\/github.com\/jwaldmann\/matchbox\/ (2014)"},{"key":"9419_CR121","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0004-3702(85)90029-3","volume":"26","author":"C Walther","year":"1985","unstructured":"Walther, C.: A mechanical solution of schubert\u2019s steamroller by many-sorted resolution. Aritif. Intell. 26, 217\u2013224 (1985)","journal-title":"Aritif. Intell."},{"issue":"2","key":"9419_CR122","doi-asserted-by":"crossref","first-page":"105","DOI":"10.2307\/2266241","volume":"17","author":"H Wang","year":"1952","unstructured":"Wang, H.: Logic of many-sorted theories. J. Symb. Logic 17(2), 105\u2013116 (1952)","journal-title":"J. Symb. Logic"},{"key":"9419_CR123","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H Zantema","year":"1994","unstructured":"Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17, 23\u201350 (1994)","journal-title":"J. Symb. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9419-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9419-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9419-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T03:54:32Z","timestamp":1750564472000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9419-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,12]]},"references-count":123,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,4]]}},"alternative-id":["9419"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9419-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,7,12]]}}}