{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T15:38:28Z","timestamp":1725982708632},"publisher-location":"Berlin, Heidelberg","reference-count":139,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662576687"},{"type":"electronic","value":"9783662576694"}],"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-662-57669-4_2","type":"book-chapter","created":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T08:48:51Z","timestamp":1530002931000},"page":"25-60","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Symbolic Reasoning Methods in Rewriting Logic and Maude"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,27]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63139-4_1","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M Alpuente","year":"2017","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: Partial evaluation of order-sorted equational programs modulo axioms. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 3\u201320. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63139-4_1"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.ic.2014.01.006","volume":"235","author":"M Alpuente","year":"2014","unstructured":"Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. 235, 98\u2013136 (2014)","journal-title":"Inf. Comput."},{"issue":"46","key":"2_CR3","doi-asserted-by":"publisher","first-page":"4608","DOI":"10.1016\/j.tcs.2009.07.037","volume":"410","author":"M Alpuente","year":"2009","unstructured":"Alpuente, M., Escobar, S., Iborra, J.: Termination of narrowing revisited. Theor. Comput. Sci. 410(46), 4608\u20134625 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"2_CR4","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1093\/jigpal\/jzq009","volume":"19","author":"M Alpuente","year":"2011","unstructured":"Alpuente, M., Escobar, S., Iborra, J.: Modular termination of basic narrowing and equational unification. Log. J. IGPL 19(6), 731\u2013762 (2011)","journal-title":"Log. J. IGPL"},{"issue":"1","key":"2_CR5","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4:1\u20134:51 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/10720246_8","volume-title":"Recent Advances in AI Planning","author":"A Armando","year":"2000","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS (LNAI), vol. 1809, pp. 97\u2013108. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10720246_8"},{"issue":"2","key":"2_CR7","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"key":"2_CR8","first-page":"48","volume":"44","author":"A Arusoaie","year":"2015","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V.: Symbolic execution based on language transformation. Comput. Lang. Syst. Struct. 44, 48\u201371 (2015)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","volume-title":"Automated Deduction\u2014CADE-18","author":"G Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Korni\u0142owicz, A., Sebastiani, R.: A SAT based approach for solving formulas over Boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 195\u2013210. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_17"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","volume-title":"Handbook of Automated Reasoning","author":"Franz Baader","year":"2001","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning. Elsevier (1999)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Baader, F., Siekmann, J.H.: Unification theory. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, pp. 41\u2013126. Oxford University Press (1994)","DOI":"10.1093\/oso\/9780198537465.003.0002"},{"key":"2_CR12","unstructured":"Bae, K.: Rewriting-based model checking methods. Ph.D. thesis, University of Illinois at Urbana-Champaign (2014)"},{"key":"2_CR13","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Rewriting Techniques and Applications (RTA 2013). LIPIcs, vol. 21, pp. 81\u201396. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-319-12904-4_6","volume-title":"Rewriting Logic and Its Applications","author":"K Bae","year":"2014","unstructured":"Bae, K., Meseguer, J.: Infinite-state model checking of LTLR formulas using narrowing. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 113\u2013129. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_6"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-08918-8_5","volume-title":"Rewriting and Typed Lambda Calculi","author":"K Bae","year":"2014","unstructured":"Bae, K., Meseguer, J.: Predicate abstraction of rewrite theories. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 61\u201376. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_5"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.scico.2014.02.006","volume":"99","author":"K Bae","year":"2015","unstructured":"Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193\u2013234 (2015)","journal-title":"Sci. Comput. Program."},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-319-68034-7_5","volume-title":"Formal Aspects of Component Software","author":"K Bae","year":"2017","unstructured":"Bae, K., Rocha, C.: Guarded terms for rewriting modulo SMT. In: Proen\u00e7a, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 78\u201397. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68034-7_5"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"CW Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 236\u2013249. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_18"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/1013560.1013566","volume":"5","author":"D Basin","year":"2004","unstructured":"Basin, D., Clavel, M., Meseguer, J.: Rewriting logic as a metalogical framework. ACM Trans. Comput. Log. 5, 528\u2013576 (2004)","journal-title":"ACM Trans. Comput. Log."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Basin, D., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: Ray, I., Li, N., Kruegel, C. (eds.) Proceedings of the 2015 ACM SIGSAC Conference on Computer and Communications Security, pp. 1144\u20131155. ACM (2015)","DOI":"10.1145\/2810103.2813662"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b11968","volume-title":"CASL User Manual - Introduction to Using the Common Algebraic Specification Language","year":"2004","unstructured":"Bidoit, M., Mosses, P.D. (eds.): CASL User Manual - Introduction to Using the Common Algebraic Specification Language. LNCS, vol. 2900. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/b11968"},{"issue":"1","key":"2_CR22","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1093\/logcom\/exm055","volume":"18","author":"MP Bonacina","year":"2008","unstructured":"Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial $$\\cal{T}$$T-satisfiability procedures. J. Log. Comput. 18(1), 77\u201396 (2008)","journal-title":"J. Log. Comput."},{"key":"2_CR23","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0304-3975(01)00358-9","volume":"285","author":"P Borovansk\u00fd","year":"2002","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H., Moreau, P.E.: ELAN from a rewriting logic point of view. Theor. Comput. Sci. 285, 155\u2013185 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR24","volume-title":"A Computational Logic","author":"R Boyer","year":"1980","unstructured":"Boyer, R., Moore, J.: A Computational Logic. Academic Press, Cambridge (1980)"},{"issue":"1\u20133","key":"2_CR25","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-11486-1_35","volume-title":"Perspectives of Systems Informatics","author":"PE Bulychev","year":"2010","unstructured":"Bulychev, P.E., Kostylev, E.V., Zakharov, V.A.: Anti-unification algorithms and their applications in program analysis. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 413\u2013423. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11486-1_35"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55034-8","volume-title":"A Resolution Principle for a Logic with Restricted Quantifiers","year":"1991","unstructured":"B\u00fcrckert, H.-J. (ed.): A Resolution Principle for a Logic with Restricted Quantifiers. LNCS, vol. 568. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-55034-8"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-28869-2_6","volume-title":"Programming Languages and Systems","author":"R Chadha","year":"2012","unstructured":"Chadha, R., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 108\u2013127. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_6"},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.scico.2015.06.001","volume":"112","author":"A Cholewa","year":"2015","unstructured":"Cholewa, A., Escobar, S., Meseguer, J.: Constrained narrowing for conditional equational theories modulo axioms. Sci. Comput. Program. 112, 24\u201357 (2015)","journal-title":"Sci. Comput. Program."},{"key":"2_CR30","unstructured":"Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, CS Dept. University of Illinois at Urbana-Champaign, February 2014. http:\/\/hdl.handle.net\/2142\/47117"},{"key":"2_CR31","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":"2","key":"2_CR32","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/BF00243207","volume":"3","author":"AG Cohn","year":"1987","unstructured":"Cohn, A.G.: A more expressive formulation of many sorted logic. J. Autom. Reason. 3(2), 113\u2013200 (1987)","journal-title":"J. Autom. Reason."},{"issue":"2\u20133","key":"2_CR33","first-page":"89","volume":"3","author":"AG Cohn","year":"1989","unstructured":"Cohn, A.G.: Taxonomic reasoning with many-sorted logics. Artif. Intell. Rev. 3(2\u20133), 89\u2013128 (1989)","journal-title":"Artif. Intell. Rev."},{"key":"2_CR34","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007). http:\/\/www.grappa.univ-lille3.fr\/tata , Accessed 12 Oct 2007"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1007\/BFb0032066","volume-title":"Automata, Languages and Programming","author":"H Comon","year":"1990","unstructured":"Comon, H.: Equational formulas in order-sorted algebras. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 674\u2013688. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032066"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_22"},{"key":"2_CR37","doi-asserted-by":"publisher","DOI":"10.1142\/3163","volume-title":"Language Prototyping: An Algebraic Specification Approach","author":"A Deursen van","year":"1996","unstructured":"van Deursen, A., Heering, J., Klint, P.: Language Prototyping: An Algebraic Specification Approach. World Scientific, Singapore (1996)"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-662-54455-6_6","volume-title":"Principles of Security and Trust","author":"J Dreier","year":"2017","unstructured":"Dreier, J., Dum\u00e9nil, C., Kremer, S., Sasse, R.: Beyond subterm-convergent equational theories in automated verification of stateful protocols. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 117\u2013140. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_6"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R.: Automated unbounded verification of stateful cryptographic protocols with exclusive OR. In: Accepted at Computer Security Foundations (CSF) (2018)","DOI":"10.1109\/CSF.2018.00033"},{"issue":"4","key":"2_CR40","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s10817-015-9352-2","volume":"56","author":"C Dross","year":"2016","unstructured":"Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Adding decision procedures to SMT solvers using axioms with triggers. J. Autom. Reason. 56(4), 387\u2013457 (2016)","journal-title":"J. Autom. Reason."},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Associative unification and symbolic reasoning modulo associativity in Maude. In: Preproceedings of WRLA 2018, Thessaloniki, Greece, April 2018. (Distributed in Electronic Form by the ETAPS 2018 Organizers). Proceedings version to appear in LNCS","DOI":"10.1007\/978-3-319-99840-4_6"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J., Rocha, C.: Proving ground confluence of equational specifications modulo axioms. Technical report, CS Dept., University of Illinois at Urbana-Champaign, March 2018. http:\/\/hdl.handle.net\/2142\/99548 . Shorter version to appear in Proceedings of the WRLA 2018. Springer LNCS","DOI":"10.1007\/978-3-319-99840-4_11"},{"key":"2_CR43","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Algebraic Log. Program. 81, 816\u2013850 (2012)","journal-title":"J. Algebraic Log. Program."},{"issue":"3","key":"2_CR44","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10817-010-9200-3","volume":"48","author":"M Echenim","year":"2012","unstructured":"Echenim, M., Peltier, N.: An instantiation scheme for satisfiability modulo theories. J. Autom. Reason. 48(3), 293\u2013362 (2012)","journal-title":"J. Autom. Reason."},{"key":"2_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-38574-2_16","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Erbatur","year":"2013","unstructured":"Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C.A., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 231\u2013248. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_16"},{"key":"2_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"2_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-16310-4_5","volume-title":"Rewriting Logic and Its Applications","author":"S Escobar","year":"2010","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 52\u201368. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16310-4_5"},{"key":"2_CR48","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.ic.2014.07.007","volume":"238","author":"S Escobar","year":"2014","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL protocol analyzer. Inf. Comput. 238, 157\u2013186 (2014)","journal-title":"Inf. Comput."},{"key":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-73449-9_13","volume-title":"Term Rewriting and Applications","author":"S Escobar","year":"2007","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153\u2013168. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73449-9_13"},{"key":"2_CR50","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebraic Log. Program. 81, 898\u2013928 (2012)","journal-title":"J. Algebraic Log. Program."},{"key":"2_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-540-27813-9_46","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2004","unstructured":"Farzan, A., Chen, F., Meseguer, J., Ro\u015fu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 501\u2013505. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_46"},{"key":"2_CR52","unstructured":"Fay, M.: First-order unification in an equational theory. In: Proceedings of the 4th Workshop on Automated Deduction, pp. 161\u2013167 (1979)"},{"key":"2_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J-C Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue*B, H., Shankar, N.: ICS: integrated Canonizer and solver? In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 246\u2013249. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_22"},{"key":"2_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355\u2013367. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_34"},{"issue":"1\u20133","key":"2_CR55","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0004-3702(91)90009-9","volume":"49","author":"AM Frisch","year":"1991","unstructured":"Frisch, A.M.: The substitutional framework for sorted deduction: fundamental results on hybrid reasoning. Artif. Intell. 49(1\u20133), 161\u2013198 (1991)","journal-title":"Artif. Intell."},{"key":"2_CR56","volume-title":"CafeOBJ Report","author":"K Futatsugi","year":"1998","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, Singapore (1998)"},{"key":"2_CR57","doi-asserted-by":"crossref","unstructured":"Gallagher, J.P.: Tutorial on specialisation of logic programs. In: Proceedings of the 1993 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 1993, pp. 88\u201398. ACM, New York (1993)","DOI":"10.1145\/154630.154640"},{"issue":"2&3","key":"2_CR58","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"JH Gallier","year":"1989","unstructured":"Gallier, J.H., Snyder, W.: Complete sets of transformations for general E-unification. Theor. Comput. Sci. 67(2&3), 203\u2013260 (1989)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR59","doi-asserted-by":"crossref","unstructured":"Garavel, H., Tabikh, M.A., Arrada, I.S.: Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages. In: Preproceedings of WRLA 2018, Thessaloniki, Greece, April 2018. (Distributed in electronic form by the ETAPS 2018 Organizers). Proceedings version to appear in LNCS","DOI":"10.1007\/978-3-319-99840-4_1"},{"issue":"2","key":"2_CR60","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0743-1066(84)90004-9","volume":"1","author":"J Goguen","year":"1984","unstructured":"Goguen, J., Meseguer, J.: Equality, types, modules and (why not?) generics for logic programming. J. Log. Program. 1(2), 179\u2013210 (1984)","journal-title":"J. Log. Program."},{"key":"2_CR61","first-page":"417","volume-title":"Research Directions in Object-Oriented Programming","author":"J Goguen","year":"1987","unstructured":"Goguen, J., Meseguer, J.: Unifying functional, object-oriented and relational programming with logical semantics. In: Shriver, B., Wegner, P. (eds.) Research Directions in Object-Oriented Programming, pp. 417\u2013477. MIT Press, Cambridge (1987)"},{"key":"2_CR62","doi-asserted-by":"publisher","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. Theor. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR63","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-1-4757-6541-0_1","volume-title":"Software Engineering with OBJ: Algebraic Specification in Action","author":"J Goguen","year":"2000","unstructured":"Goguen, J., 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, pp. 3\u2013167. Kluwer, Dordrecht (2000)"},{"key":"2_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-14054-4_8","volume-title":"Security Standardisation Research","author":"A Gonz\u00e1lez-Burgue\u00f1o","year":"2014","unstructured":"Gonz\u00e1lez-Burgue\u00f1o, A., Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: Analysis of the IBM CCA security API protocols in Maude-NPA. In: Chen, L., Mitchell, C. (eds.) SSR 2014. LNCS, vol. 8893, pp. 111\u2013130. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-14054-4_8"},{"key":"2_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-319-27152-1_5","volume-title":"Security Standardisation Research","author":"A Gonz\u00e1lez-Burgue\u00f1o","year":"2015","unstructured":"Gonz\u00e1lez-Burgue\u00f1o, A., Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: Analysis of the PKCS#11 API using the Maude-NPA tool. In: Chen, L., Matsuo, S. (eds.) SSR 2015. LNCS, vol. 9497, pp. 86\u2013106. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-27152-1_5"},{"key":"2_CR66","doi-asserted-by":"crossref","unstructured":"Guti\u00e9rrez, R., Meseguer, J.: Variant-based decidable satisfiability in initial algebras with predicates. To appear in Proceedings of LOPSTR 2017. Springer LNCS 2018","DOI":"10.1007\/978-3-319-94460-9_18"},{"key":"2_CR67","unstructured":"Guti\u00e9rrez, R., Meseguer, J.: Variant-based decidable satisfiability in initial algebras with predicates. Technical report, University of Illinois at Urbana-Champaign, June 2017. http:\/\/hdl.handle.net\/2142\/96264"},{"issue":"2","key":"2_CR68","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/S0304-3975(96)00323-4","volume":"183","author":"AE Haxthausen","year":"1997","unstructured":"Haxthausen, A.E.: Order-sorted algebraic specifications with higher-order functions. Theor. Comput. Sci. 183(2), 157\u2013185 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11805618_5","volume-title":"Term Rewriting and Applications","author":"J Hendrix","year":"2006","unstructured":"Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional tree automata. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 50\u201365. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11805618_5"},{"key":"2_CR70","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2012.11.010","volume":"290","author":"J Hendrix","year":"2012","unstructured":"Hendrix, J., Meseguer, J.: Order-sorted equational unification revisited. Electr. Notes Theor. Comput. Sci. 290, 37\u201350 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"2_CR71","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11814771_14","volume-title":"Automated Reasoning","author":"J Hendrix","year":"2006","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151\u2013155. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_14"},{"key":"2_CR72","unstructured":"Hendrix, J.D.: Decision procedures for equationally based reasoning. Ph.D. thesis, University of Illinois at Urbana-Champaign (2008). http:\/\/hdl.handle.net\/2142\/10967"},{"key":"2_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction Les Arcs, France, July 8\u201311, 1980","author":"J-M Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 318\u2013334. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10009-1_25"},{"key":"2_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0036921","volume-title":"Automata, Languages and Programming","author":"J-P Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 361\u2013373. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/BFb0036921"},{"key":"2_CR75","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"JP Jouannaud","year":"1986","unstructured":"Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15, 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"issue":"7\u20138","key":"2_CR76","doi-asserted-by":"publisher","first-page":"929","DOI":"10.1016\/j.jlap.2012.06.002","volume":"81","author":"M Katelman","year":"2012","unstructured":"Katelman, M., Keller, S., Meseguer, J.: Rewriting semantics of production rule sets. J. Log. Algebraic Program. 81(7\u20138), 929\u2013956 (2012)","journal-title":"J. Log. Algebraic Program."},{"key":"2_CR77","unstructured":"Kirchner, C.: Order-sorted equational unification. Technical report 954, INRIA Lorraine & LORIA, Nancy, France (1988)"},{"key":"2_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1007\/11560647_39","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"H Kirchner","year":"2005","unstructured":"Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.K.: On superposition-based satisfiability procedures and their combination. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 594\u2013608. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560647_39"},{"key":"2_CR79","first-page":"429","volume":"7","author":"E Kitzelmann","year":"2006","unstructured":"Kitzelmann, E., Schmid, U.: Inductive synthesis of functional programs: an explanation based generalization approach. J. Mach. Learn. Res. 7, 429\u2013454 (2006)","journal-title":"J. Mach. Learn. Res."},{"key":"2_CR80","unstructured":"Kutsia, T., Levy, J., Villaret, M.: Anti-unification for unranked terms and hedges. In: Schmidt-Schau\u00df, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011. LIPIcs, Novi Sad, Serbia, 30 May\u20131 June 2011, vol. 10, pp. 219\u2013234. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"issue":"3","key":"2_CR81","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/BF00243794","volume":"3","author":"JL Lassez","year":"1987","unstructured":"Lassez, J.L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reason. 3(3), 301\u2013317 (1987)","journal-title":"J. Autom. Reason."},{"issue":"1\u20134","key":"2_CR82","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/A:1018952121991","volume":"28","author":"J Lu","year":"2000","unstructured":"Lu, J., Mylopoulos, J., Harao, M., Hagiya, M.: Higher order generalization and its application in program verification. Ann. Math. Artif. Intell. 28(1\u20134), 107\u2013126 (2000)","journal-title":"Ann. Math. Artif. Intell."},{"key":"2_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-319-23165-5_21","volume-title":"Logic, Rewriting, and Concurrency","author":"D Lucanu","year":"2015","unstructured":"Lucanu, D., Rusu, V., Arusoaie, A., Nowak, D.: Verifying reachability-logic properties on rewriting-logic specifications. In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 451\u2013474. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23165-5_21"},{"issue":"1","key":"2_CR84","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. Algebric Methods Program. 85(1), 67\u201397 (2016)","journal-title":"J. Log. Algebric Methods Program."},{"key":"2_CR85","doi-asserted-by":"crossref","unstructured":"Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of the LICS 2002, p. 7. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029813"},{"key":"2_CR86","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-73595-3_22","volume-title":"Automated Deduction \u2013 CADE-21","author":"C Lynch","year":"2007","unstructured":"Lynch, C., Tran, D.-K.: Automatic decidability and combinability revisited. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 328\u2013344. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_22"},{"key":"2_CR87","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1093\/logcom\/6.4.541","volume":"6","author":"N Mart\u00ed-Oliet","year":"1996","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Inclusions and subtypes II: higher-order case. J. Log. Comput. 6, 541\u2013572 (1996)","journal-title":"J. Log. Comput."},{"key":"2_CR88","first-page":"1","volume-title":"Handbook of Philosophical Logic","author":"N Mart\u00ed-Oliet","year":"2002","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn, pp. 1\u201387. Kluwer Academic Publishers, Dordrecht (2002). First published as SRI Technical report SRI-CSL-93-05, August 1993","edition":"2"},{"issue":"7\u20138","key":"2_CR89","doi-asserted-by":"publisher","first-page":"782","DOI":"10.1016\/j.jlap.2012.06.001","volume":"81","author":"N Mart\u00ed-Oliet","year":"2012","unstructured":"Mart\u00ed-Oliet, N., Palomino, M., Verdejo, A.: Rewriting logic bibliography by topic: 1990\u20132011. J. Log. Algebric Program. 81(7\u20138), 782\u2013815 (2012). https:\/\/doi.org\/10.1016\/j.jlap.2012.06.001","journal-title":"J. Log. Algebric Program."},{"key":"2_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"2_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-540-68679-8_22","volume-title":"Concurrency, Graphs and Models","author":"J Meseguer","year":"2008","unstructured":"Meseguer, J.: The temporal logic of rewriting: a gentle introduction. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 354\u2013382. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68679-8_22"},{"issue":"1\u20132","key":"2_CR92","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. J. High.-Order Symb. Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"J. High.-Order Symb. Comput."},{"issue":"1","key":"2_CR93","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR94","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":"2_CR95","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. Algebraic Log. Program. 81, 721\u2013781 (2012)","journal-title":"J. Algebraic Log. Program."},{"key":"2_CR96","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.12.026","volume":"672","author":"J Meseguer","year":"2017","unstructured":"Meseguer, J.: Strict coherence of conditional rewriting modulo axioms. Theor. Comput. Sci. 672, 1\u201335 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR97","unstructured":"Meseguer, J.: Generalized rewrite theories and coherence completion. Technical report, University of Illinois Computer Science Department, March 2018. http:\/\/hdl.handle.net\/2142\/99546 . Shorter version to appear in Proceedings of WRLA 2018, Springer LNCS"},{"key":"2_CR98","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2017.09.001","volume":"154","author":"J Meseguer","year":"2018","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3\u201341 (2018)","journal-title":"Sci. Comput. Program."},{"key":"2_CR99","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1016\/S0747-7171(89)80036-7","volume":"8","author":"J Meseguer","year":"1989","unstructured":"Meseguer, J., Goguen, J., Smolka, G.: Order-sorted unification. J. Symb. Comput. 8, 383\u2013413 (1989)","journal-title":"J. Symb. Comput."},{"key":"2_CR100","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.ic.2013.08.004","volume":"231","author":"J Meseguer","year":"2013","unstructured":"Meseguer, J., Rosu, G.: The rewriting logic semantics project: a progress report. Inf. Comput. 231, 38\u201369 (2013)","journal-title":"Inf. Comput."},{"issue":"3","key":"2_CR101","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s00165-017-0415-5","volume":"29","author":"J Meseguer","year":"2017","unstructured":"Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Formal Asp. Comput. 29(3), 423\u2013452 (2017)","journal-title":"Formal Asp. Comput."},{"issue":"4","key":"2_CR102","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1023\/A:1026551132647","volume":"13","author":"T\u00c6 Mogensen","year":"2000","unstructured":"Mogensen, T.\u00c6.: Glossary for partial evaluation and related topics. High.-Order Symbol. Comput. 13(4), 355\u2013368 (2000)","journal-title":"High.-Order Symbol. Comput."},{"key":"2_CR103","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b96103","volume-title":"Casl Reference Manual. The Complete Documentation of the Common Algebraic Specification Language","year":"2004","unstructured":"Mosses, P.D. (ed.): Casl Reference Manual. The Complete Documentation of the Common Algebraic Specification Language. LNCS, vol. 2960. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/b96103"},{"key":"2_CR104","unstructured":"de Moura, L., Rue\u00df, H.: Lemmas on demand for satisfiability solvers. In: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002), May 2002"},{"issue":"1\u20132","key":"2_CR105","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/S0004-3702(99)00067-3","volume":"114","author":"S Muggleton","year":"1999","unstructured":"Muggleton, S.: Inductive logic programming: issues, results and the challenge of learning language in logic. Artif. Intell. 114(1\u20132), 283\u2013296 (1999)","journal-title":"Artif. Intell."},{"issue":"2","key":"2_CR106","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"2_CR107","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"2_CR108","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Unification and anti-unification in the calculus of constructions. In: Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, 15\u201318 July 1991, pp. 74\u201385. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151632"},{"key":"2_CR109","unstructured":"Plotkin, G.: A note on inductive generalization. In: Machine Intelligence, vol. 5, pp. 153\u2013163. Edinburgh University Press (1970)"},{"key":"2_CR110","unstructured":"Popplestone, R.: An experiment in automatic induction. In: Machine Intelligence, vol. 5, pp. 203\u2013215. Edinburgh University Press (1969)"},{"key":"2_CR111","first-page":"135","volume":"5","author":"J Reynolds","year":"1970","unstructured":"Reynolds, J.: Transformational systems and the algebraic structure of atomic formulas. Mach. Intell. 5, 135\u2013151 (1970)","journal-title":"Mach. Intell."},{"key":"2_CR112","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12, 23\u201341 (1965)","journal-title":"J. Assoc. Comput. Mach."},{"key":"2_CR113","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-642-22944-2_22","volume-title":"Algebra and Coalgebra in Computer Science","author":"C Rocha","year":"2011","unstructured":"Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314\u2013328. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22944-2_22"},{"key":"2_CR114","unstructured":"Rocha, C.: Symbolic reachability analysis for rewrite theories. Ph.D. thesis, University of Illinois at Urbana-Champaign (2012)"},{"key":"2_CR115","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1007\/978-3-642-54624-2_30","volume-title":"Specification, Algebra, and Software","author":"C Rocha","year":"2014","unstructured":"Rocha, C., Meseguer, J.: Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 603\u2013629. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54624-2_30"},{"key":"2_CR116","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.A.: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86, 269\u2013297 (2017)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"6","key":"2_CR117","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Rosu","year":"2010","unstructured":"Rosu, G., Serbanuta, T.: An overview of the K semantic framework. J. Log. Algebraic Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebraic Program."},{"key":"2_CR118","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Proceedings of the CSF 2012, pp. 78\u201394. IEEE (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"2_CR119","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Sasse, R., Cremers, C., Basin, D.: Automated verification of group key agreement protocols. In: Proceedings of the 2014 IEEE Symposium on Security and Privacy, SP 2014, pp. 179\u2013194. IEEE Computer Society, Washington, D.C. (2014)","DOI":"10.1109\/SP.2014.19"},{"key":"2_CR120","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/3-540-16780-3_118","volume-title":"8th International Conference on Automated Deduction","author":"M Schmidt-Schauss","year":"1986","unstructured":"Schmidt-Schauss, M.: Unification in many-sorted equational theories. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 538\u2013552. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16780-3_118"},{"key":"2_CR121","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0024065","volume-title":"Computational Aspects of an Order-Sorted Logic with Term Declarations","year":"1989","unstructured":"Schmidt-Schau\u00df, M. (ed.): Computational Aspects of an Order-Sorted Logic with Term Declarations. LNCS, vol. 395. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0024065"},{"issue":"1","key":"2_CR122","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"issue":"3\/4","key":"2_CR123","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"JH Siekmann","year":"1989","unstructured":"Siekmann, J.H.: Unification theory. J. Symb. Comput. 7(3\/4), 207\u2013274 (1989)","journal-title":"J. Symb. Comput."},{"key":"2_CR124","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/j.jlamp.2017.12.006","volume":"96","author":"S Skeirik","year":"2018","unstructured":"Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. J. Log. Algebric Methods Program. 96, 81\u2013110 (2018)","journal-title":"J. Log. Algebric Methods Program."},{"key":"2_CR125","unstructured":"Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Technical report, University of Illinois Computer Science Department, March 2017. http:\/\/hdl.handle.net\/2142\/95770 . Shorter version to appear in Proceedings of LOPSTR 2107, Springer LNCS 2018"},{"issue":"4","key":"2_CR126","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"JR Slagle","year":"1974","unstructured":"Slagle, J.R.: Automated theorem-proving for theories with simplifiers commutativity, and associativity. J. ACM 21(4), 622\u2013642 (1974)","journal-title":"J. ACM"},{"issue":"3\/4","key":"2_CR127","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/S0747-7171(89)80016-1","volume":"7","author":"G Smolka","year":"1989","unstructured":"Smolka, G., A\u00eft-Kaci, H.: Inheritance hierarchies: semantics and unification. J. Symb. Comput. 7(3\/4), 343\u2013370 (1989)","journal-title":"J. Symb. Comput."},{"key":"2_CR128","first-page":"297","volume-title":"Resolution of Equations in Algebraic Structures","author":"G Smolka","year":"1989","unstructured":"Smolka, G., Nutt, W., Goguen, J., Meseguer, J.: Order-sorted equational computation. In: Nivat, M., A\u00eft-Kaci, H. (eds.) Resolution of Equations in Algebraic Structures, vol. 2, pp. 297\u2013367. Academic Press, Cambridge (1989)"},{"key":"2_CR129","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0435-0","volume-title":"A Proof Theory for General Unification","author":"W Snyder","year":"1991","unstructured":"Snyder, W.: A Proof Theory for General Unification. Birkh\u00e4user, Boston (1991)"},{"key":"2_CR130","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-319-08918-8_29","volume-title":"Rewriting and Typed Lambda Calculi","author":"A \u015etef\u0103nescu","year":"2014","unstructured":"\u015etef\u0103nescu, A., Ciob\u00e2c\u0103, \u015e., Mereuta, R., Moore, B.M., \u015eerb\u0103nut\u0103, T.F., Ro\u015fu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 425\u2013440. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_29"},{"key":"2_CR131","doi-asserted-by":"crossref","unstructured":"Stefanescu, A., Park, D., Yuwen, S., Li, Y., Rosu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the OOPSLA 2016, pp. 74\u201391. ACM (2016)","DOI":"10.1145\/2983990.2984027"},{"key":"2_CR132","first-page":"70","volume":"36","author":"MO Stehr","year":"2000","unstructured":"Stehr, M.O.: CINNI - a generic calculus of explicit substitutions and its application to $$\\lambda $$\u03bb-, $$\\sigma $$\u03c3- and $$\\pi $$\u03c0-calculi. ENTCS 36, 70\u201392 (2000). Proceedings of the 3rd International Workshop on Rewriting Logic and Its Applications","journal-title":"ENTCS"},{"key":"2_CR133","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-39993-3_16","volume-title":"From Object-Orientation to Formal Methods","author":"M-O Stehr","year":"2004","unstructured":"Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 334\u2013375. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-39993-3_16"},{"key":"2_CR134","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45541-8_9","volume-title":"Unifying Petri Nets","author":"M-O Stehr","year":"2001","unstructured":"Stehr, M.-O., Meseguer, J., \u00d6lveczky, P.C.: Rewriting logic as a unifying framework for Petri nets. In: Ehrig, H., Padberg, J., Juh\u00e1s, G., Rozenberg, G. (eds.) Unifying Petri Nets. LNCS, vol. 2128, pp. 250\u2013303. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45541-8_9"},{"key":"2_CR135","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2014.02.005","volume":"99","author":"E Tushkanova","year":"2015","unstructured":"Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.: A rule-based system for automatic decidability and combinability. Sci. Comput. Program. 99, 3\u201323 (2015)","journal-title":"Sci. Comput. Program."},{"key":"2_CR136","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285, 487\u2013517 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"2_CR137","doi-asserted-by":"publisher","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. Artif. Intell. 26(2), 217\u2013224 (1985)","journal-title":"Artif. Intell."},{"key":"2_CR138","doi-asserted-by":"crossref","unstructured":"Yang, F., Escobar, S., Meadows, C., Meseguer, J., Narendran, P.: Theories of homomorphic encryption, unification, and the finite variant property. In: Proceedings of the PPDP 2014, pp. 123\u2013133. ACM (2014)","DOI":"10.1145\/2643135.2643154"},{"key":"2_CR139","doi-asserted-by":"crossref","unstructured":"Yang, F., Escobar, S., Meadows, C.A., Meseguer, J., Santiago, S.: Strand spaces with choice via a process algebra semantics. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP), Edinburgh, United Kingdom, 5\u20137 September 2016, pp. 76\u201389. ACM (2016)","DOI":"10.1145\/2967973.2968609"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-57669-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,7]],"date-time":"2024-07-07T18:39:20Z","timestamp":1720377560000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-57669-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783662576687","9783662576694"],"references-count":139,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-57669-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}