{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T16:33:01Z","timestamp":1743093181011,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030138370"},{"type":"electronic","value":"9783030138387"}],"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-13838-7_1","type":"book-chapter","created":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T22:15:23Z","timestamp":1550787323000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Proving Program Properties as First-Order Satisfiability"],"prefix":"10.1007","author":[{"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,2,23]]},"reference":[{"key":"1_CR1","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, New York (1998)"},{"key":"1_CR2","doi-asserted-by":"publisher","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"},{"issue":"1","key":"1_CR3","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. Theoret. Comput. Sci. 351(1), 386\u2013414 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR4","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":"1_CR5","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"1_CR6","unstructured":"Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: Proceedings of LICS 1990, pp. 242\u2013248. IEEE Press (1990)"},{"key":"1_CR7","unstructured":"Dershowitz, N., Kaplan, S., Plaisted, D.: Rewrite, rewrite, rewrite, rewrite, rewrite, \n                      \n                        \n                      \n                      $$\\ldots $$\n                     Theoret. Comput. Sci. 83, 71\u201396 (1991)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"3203","DOI":"10.1016\/j.tcs.2011.03.024","volume":"412","author":"J Endrullis","year":"2011","unstructured":"Endrullis, J., Hendriks, D.: Lazy productivity via termination. Theoret. Comput. Sci. 412, 3203\u20133225 (2011)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR9","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). \n                      https:\/\/doi.org\/10.1007\/BFb0014969"},{"key":"1_CR10","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 available at \n                      http:\/\/zenon.dsic.upv.es\/ages\/"},{"key":"1_CR11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574","volume-title":"Model Theory","author":"W Hodges","year":"1993","unstructured":"Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)"},{"key":"1_CR12","unstructured":"Kim, S., Zhang, H.: ModGen: theorem proving by model generation. In: Proceedings of AAAI 1994, pp. 162\u2013167. AAAI Press\/MIT Press (1994)"},{"key":"1_CR13","volume-title":"Mathematical Logic","author":"SC Kleene","year":"1967","unstructured":"Kleene, S.C.: Mathematical Logic. Wiley, Hoboken (1967). (Dover 2002)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-319-94460-9_11","volume-title":"Logic-Based Program Synthesis and Transformation","author":"S Lucas","year":"2018","unstructured":"Lucas, S.: Analysis of rewriting-based systems as first-order theories. In: Fioravanti, F., Gallagher, J.P. (eds.) LOPSTR 2017. LNCS, vol. 10855, pp. 180\u2013197. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-94460-9_11"},{"issue":"4","key":"1_CR15","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":"1_CR16","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)","journal-title":"Inf. Process. Lett."},{"key":"1_CR17","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). \n                      http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"1_CR18","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":"1_CR19","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). \n                      https:\/\/doi.org\/10.1007\/978-1-4757-3661-8"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-1-4684-3384-5_3","volume-title":"Logic and Data Bases","author":"Raymond Reiter","year":"1978","unstructured":"Reiter, R.: On closed world data bases. In: Logic and Data Bases, pp. 119\u2013140. Plenum Press, New York (1978)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-40970-2_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"G Reger","year":"2016","unstructured":"Reger, G., Suda, M., Voronkov, A.: Finding finite models in multi-sorted first-order logic. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 323\u2013341. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40970-2_20"},{"key":"1_CR22","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, Oxford (1991)"},{"issue":"2","key":"1_CR23","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)","journal-title":"J. Symbolic Logic"},{"key":"1_CR24","first-page":"308","volume-title":"Proceedings of CADE 1996","author":"J Zhang","year":"1996","unstructured":"Zhang, J., Zhang, H.: Generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 308\u2013312. Springer, New York (1996)"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-13838-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T07:33:59Z","timestamp":1558337639000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-13838-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030138370","9783030138387"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-13838-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Frankfurt\/Main","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 September 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2018","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":"lopstr2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ppdp-lopstr-18.cs.uni-frankfurt.de\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}