{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:21:20Z","timestamp":1761920480503,"version":"3.37.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319944593"},{"type":"electronic","value":"9783319944609"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94460-9_11","type":"book-chapter","created":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T11:36:38Z","timestamp":1531136198000},"page":"180-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Analysis of Rewriting-Based Systems as First-Order Theories"],"prefix":"10.1007","author":[{"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,10]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-642-40885-4_22","volume-title":"Frontiers of Combining Systems","author":"T Aoto","year":"2013","unstructured":"Aoto, T.: Disproving confluence of term rewriting systems by interpretation and ordering. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 311\u2013326. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_22"},{"key":"11_CR2","doi-asserted-by":"publisher","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":"11_CR3","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"JA Bergstra","year":"1986","unstructured":"Bergstra, J.A., Klop, J.W.: Conditional rewrite rules: confluence and termination. J. Comput. Syst. Sci. 32, 323\u2013362 (1986)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"11_CR4","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"351","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 351(1), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR5","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, New York (1973)"},{"key":"11_CR6","unstructured":"Clark, K.L.: Predicate logic as a computational formalism. Ph.D. thesis, Research Monograph 79\/59 TOC, Department of Computing, Imperial College of Science, and Technology, University of London, December 1979"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"issue":"11","key":"11_CR8","first-page":"1618","volume":"12","author":"M Clavel","year":"2006","unstructured":"Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. J. Univ. Comput. Sci. 12(11), 1618\u20131650 (2006)","journal-title":"J. Univ. Comput. Sci."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: Proceedings of LICS 1990, pp. 242\u2013248. IEEE Press (1990)","DOI":"10.1109\/LICS.1990.113750"},{"key":"11_CR10","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. J. Symb. Comput. 3, 69\u2013115 (1987)","journal-title":"J. Symb. Comput."},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/0304-3975(90)90064-O","volume":"75","author":"N Dershowitz","year":"1990","unstructured":"Dershowitz, N., Okada, M.: A rationale for conditional equational programming. Theor. Comput. Sci. 75, 111\u2013138 (1990)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-45085-6_27","volume-title":"Automated Deduction \u2013 CADE-19","author":"J-M Gaillourdet","year":"2003","unstructured":"Gaillourdet, J.-M., Hillenbrand, T., L\u00f6chner, B., Spies, H.: The new WALDMEISTER loop at work. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 317\u2013321. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_27"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-540-89439-1_47","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"JP Gallagher","year":"2008","unstructured":"Gallagher, J.P., Rosendahl, M.: Approximating term rewriting systems: a horn clause specification and its implementation. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 682\u2013696. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_47"},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s002000100063","volume":"12","author":"J Giesl","year":"2001","unstructured":"Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39\u201372 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0014969","volume-title":"TAPSOFT \u201987","author":"JA Goguen","year":"1987","unstructured":"Goguen, J.A., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol. 250, pp. 1\u201322. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/BFb0014969"},{"key":"11_CR16","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 2016, pp. 215\u2013230 (2016). Tool http:\/\/zenon.dsic.upv.es\/ages\/"},{"key":"11_CR17","volume-title":"A Shorter Model Theory","author":"W Hodges","year":"1997","unstructured":"Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997)"},{"key":"11_CR18","unstructured":"Lucas, S., Guti\u00e9rrez, R.: A semantic criterion for proving infeasibility in conditional rewriting. In: Proceedings of IWC 2017, pp. 15\u201320 (2017)"},{"issue":"4","key":"11_CR19","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s10817-017-9419-3","volume":"60","author":"S Lucas","year":"2018","unstructured":"Lucas, S., Guti\u00e9rrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465\u2013501 (2018)","journal-title":"J. Autom. Reason."},{"key":"11_CR20","doi-asserted-by":"publisher","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. Inf. Process. Lett. 95, 446\u2013453 (2005)","journal-title":"Inf. Process. Lett."},{"key":"11_CR21","doi-asserted-by":"publisher","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. Algebraic Methods Program. 86, 236\u2013268 (2017)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-319-13770-4_3","volume-title":"Artificial Intelligence and Symbolic Computation","author":"S Lucas","year":"2014","unstructured":"Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Aranda-Corral, G.A., Calmet, J., Mart\u00edn-Mateos, F.J. (eds.) AISC 2014. LNCS (LNAI), vol. 8884, pp. 9\u201320. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13770-4_3"},{"issue":"1","key":"11_CR23","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.jlamp.2015.06.001","volume":"85","author":"S Lucas","year":"2016","unstructured":"Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebraic Methods Program. 85(1), 67\u201397 (2016)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-319-17822-6_7","volume-title":"Logic-Based Program Synthesis and Transformation","author":"S Lucas","year":"2015","unstructured":"Lucas, S., Meseguer, J., Guti\u00e9rrez, R.: Extending the 2D dependency pair framework for conditional term rewriting systems. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 113\u2013130. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17822-6_7"},{"key":"11_CR25","volume-title":"Introduction to Mathematical Logic","author":"E Mendelson","year":"1997","unstructured":"Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, Boca Raton (1997)","edition":"4"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-64299-4_26"},{"key":"11_CR27","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81, 721\u2013781 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"11_CR28","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-1-4757-3661-8"},{"key":"11_CR29","volume-title":"Natural Deduction: A Proof-Theoretical Study","author":"D Prawitz","year":"2006","unstructured":"Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Dover, Mineola (2006)"},{"key":"11_CR30","unstructured":"Rapp, F., Middeldorp, A.: Automating the first-order theory of rewriting for left-linear right-ground rewrite systems. In: Proceedings of FSCD 2016, LIPIcs, vol. 52, pp. 36:1\u201336:12 (2016). Article No. 36"},{"key":"11_CR31","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":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-319-08918-8_31","volume-title":"Rewriting and Typed Lambda Calculi","author":"T Sternagel","year":"2014","unstructured":"Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 456\u2013465. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_31"},{"key":"11_CR33","unstructured":"Sternagel, T., Middeldorp, A.: Infefasible conditional critical pairs. In: Proceedings of IWC 2015, pp. 13\u201318 (2015)"},{"key":"11_CR34","unstructured":"Sternagel, C., Sternagel, T.: Certifying confluence of almost orthogonal CTRSs via exact tree automata completion. In: Proceedings of FSCD 2016, LIPIcs, vol. 52, pp. 85:1\u201385:16 (2016). Article No. 85"},{"key":"11_CR35","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/S0304-3975(98)00083-8","volume":"208","author":"R Treinen","year":"1998","unstructured":"Treinen, R.: The first-order theory of linear one-step rewriting is undecidable. Theor. Comput. Sci. 208, 179\u2013190 (1998)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"11_CR36","doi-asserted-by":"publisher","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"}],"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-319-94460-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T10:22:46Z","timestamp":1571566966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94460-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319944593","9783319944609"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94460-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}