{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:50:50Z","timestamp":1781927450660,"version":"3.54.5"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030294359","type":"print"},{"value":"9783030294366","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-29436-6_17","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"287-299","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Automatic Generation of Logical Models with AGES"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3984-2868","authenticated-orcid":false,"given":"Ra\u00fal","family":"Guti\u00e9rrez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9923-2108","authenticated-orcid":false,"given":"Salvador","family":"Lucas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-17796-5_12","volume-title":"Algebraic Methodology and Software Technology","author":"B Alarc\u00f3n","year":"2011","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201\u2013208. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-17796-5_12"},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"Bau, A., Lohrey, M., N\u00f6th, E., Waldmann, J.: Compression of rewriting systems for termination analysis. In: van Raamsdonk, F. (ed.) Proceedings of the 24th International Conference on Rewriting Techniques and Applications, RTA 2013, LIPICS, vol. 21, pp. 97\u2013112 (2013). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.97","DOI":"10.4230\/LIPIcs.RTA.2013.97"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer Aided Verification","author":"M Bofill","year":"2008","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_27"},{"key":"17_CR4","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., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"issue":"2\u20133","key":"17_CR6","doi-asserted-by":"publisher","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. Reasoning 40(2\u20133), 195\u2013220 (2008). https:\/\/doi.org\/10.1007\/s10817-007-9087-9","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"17_CR7","doi-asserted-by":"publisher","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. Reasoning 37(3), 155\u2013203 (2006). https:\/\/doi.org\/10.1007\/s10817-006-9057-7","journal-title":"J. Autom. Reasoning"},{"key":"17_CR8","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":"17_CR9","doi-asserted-by":"publisher","unstructured":"Lucas, S.: Using Well-Founded Relations for Proving Operational Termination. J. Autom. Reasoning (2019). https:\/\/doi.org\/10.1007\/s10817-019-09514-2","DOI":"10.1007\/s10817-019-09514-2"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-13838-7_1","volume-title":"Logic-Based Program Synthesis and Transformation","author":"S Lucas","year":"2019","unstructured":"Lucas, S.: Proving program properties as first-order satisfiability. In: Mesnard, F., Stuckey, P.J. (eds.) LOPSTR 2018. LNCS, vol. 11408, pp. 3\u201321. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-13838-7_1"},{"issue":"4","key":"17_CR11","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. Reasoning 60(4), 465\u2013501 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9419-3","journal-title":"J. Autom. Reasoning"},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.ipl.2018.04.002","volume":"136","author":"S Lucas","year":"2018","unstructured":"Lucas, S., Guti\u00e9rrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90\u201395 (2018). https:\/\/doi.org\/10.1016\/j.ipl.2018.04.002","journal-title":"Inf. Process. Lett."},{"key":"17_CR13","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). https:\/\/doi.org\/10.1016\/j.ipl.2005.05.002","journal-title":"Inf. Process. Lett."},{"key":"17_CR14","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. Logical Algebraic Methods Program. 86, 236\u2013268 (2017). https:\/\/doi.org\/10.1016\/j.jlamp.2016.03.003","journal-title":"J. Logical Algebraic Methods Program."},{"key":"17_CR15","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"17_CR17","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"},{"issue":"2","key":"17_CR18","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. Symbolic Logic 17(2), 105\u2013116 (1952). https:\/\/doi.org\/10.2307\/2266241","journal-title":"J. Symbolic Logic"},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00247667","volume":"17","author":"J Zhang","year":"1996","unstructured":"Zhang, J.: Constructing finite algebras with FALCON. J. Autom. Reasoning 17, 1\u201322 (1996). https:\/\/doi.org\/10.1007\/BF00247667","journal-title":"J. Autom. Reasoning"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-61511-3_96","volume-title":"Automated Deduction \u2014 Cade-13","author":"J Zhang","year":"1996","unstructured":"Zhang, J., Zhang, H.: System description generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 308\u2013312. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_96"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:54:53Z","timestamp":1657576493000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}