{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:05:45Z","timestamp":1767927945571,"version":"3.49.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031107689","type":"print"},{"value":"9783031107696","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Equational unification and matching are fundamental mechanisms in many automated deduction applications. Supporting them efficiently for as wide as possible a class of equational theories, and in a typed manner supporting type hierarchies, benefits many applications; but this is both challenging and nontrivial. We present Maude 3.2\u2019s efficient support of these features as well as of symbolic reachability analysis of infinite-state concurrent systems based on them.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_31","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"529-540","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Equational Unification and\u00a0Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5864-8094","authenticated-orcid":false,"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9154-262X","authenticated-orcid":false,"given":"Steven","family":"Eker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3550-4781","authenticated-orcid":false,"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6576-762X","authenticated-orcid":false,"given":"Narciso","family":"Mart\u00ed-Oliet","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4779-3848","authenticated-orcid":false,"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2983-3404","authenticated-orcid":false,"given":"Rub\u00e9n","family":"Rubio","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2845-7144","authenticated-orcid":false,"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44795-4_1","volume-title":"Machine Learning: ECML 2001","author":"H A\u00eft-Kaci","year":"2003","unstructured":"A\u00eft-Kaci, H., Sasaki, Y.: An axiomatic approach to feature term generalization. In: De Raedt, L., Flach, P. (eds.) ECML 2001. LNCS (LNAI), vol. 2167, pp. 1\u201312. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44795-4_1"},{"key":"31_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-030-19570-0_11","volume-title":"Logics in Artificial Intelligence","author":"M Alpuente","year":"2019","unstructured":"Alpuente, M., Ballis, D., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: ACUOS$${}^{\\text{2 }}$$: a high-performance system for modular ACU generalization with subtyping and inheritance. In: Calimeri, F., Leone, N., Manna, M. (eds.) JELIA 2019. LNCS (LNAI), vol. 11468, pp. 171\u2013181. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-19570-0_11"},{"issue":"3\u20134","key":"31_CR3","doi-asserted-by":"publisher","first-page":"297","DOI":"10.3233\/FI-2020-1991","volume":"177","author":"M Alpuente","year":"2020","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: Order-sorted homeomorphic embedding modulo combinations of associativity and\/or commutativity axioms. Fundam. Inform. 177(3\u20134), 297\u2013329 (2020)","journal-title":"Fundam. Inform."},{"key":"31_CR4","doi-asserted-by":"publisher","first-page":"100501","DOI":"10.1016\/j.jlamp.2019.100501","volume":"110","author":"M Alpuente","year":"2020","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: A partial evaluation framework for order-sorted equational programs modulo axioms. J. Log. Algebraic Methods Program. 110, 100501 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"4","key":"31_CR5","doi-asserted-by":"publisher","first-page":"768","DOI":"10.1145\/291891.291896","volume":"20","author":"M Alpuente","year":"1998","unstructured":"Alpuente, M., Falaschi, M., Vidal, G.: Partial evaluation of functional logic programs. ACM Trans. Program. Lang. Syst. 20(4), 768\u2013844 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"31_CR6","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: RTA 2013. LIPIcs, vol. 21, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"key":"31_CR7","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":"31_CR8","doi-asserted-by":"crossref","unstructured":"Chadha, R., Cheval, V., Ciob\u00e2c\u0103, \u015e, Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1\u201323:32 (2016)","DOI":"10.1145\/2926715"},{"key":"31_CR9","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":"31_CR10","unstructured":"Clavel, M., et al.: Maude manual (version 3.2.1). SRI International, February 2022. http:\/\/maude.cs.illinois.edu"},{"key":"31_CR11","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. Lecture Notes in Computer Science, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"issue":"7","key":"31_CR12","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/79204.79210","volume":"33","author":"A Colmerauer","year":"1990","unstructured":"Colmerauer, A.: An introduction to Prolog III. Commun. ACM 33(7), 69\u201390 (1990)","journal-title":"Commun. ACM"},{"key":"31_CR13","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":"31_CR14","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 243\u2013320. North-Holland (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"31_CR15","doi-asserted-by":"publisher","first-page":"100497","DOI":"10.1016\/j.jlamp.2019.100497","volume":"110","author":"F Dur\u00e1n","year":"2020","unstructured":"Dur\u00e1n, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110, 100497 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-99840-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F Dur\u00e1n","year":"2018","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: Rusu, V. (ed.) WRLA 2018. LNCS, vol. 11152, pp. 98\u2013114. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99840-4_6"},{"key":"31_CR17","doi-asserted-by":"publisher","first-page":"100513","DOI":"10.1016\/j.jlamp.2019.100513","volume":"111","author":"F Dur\u00e1n","year":"2020","unstructured":"Dur\u00e1n, F., Meseguer, J., Rocha, C.: Ground confluence of order-sorted conditional specifications modulo axioms. J. Log. Algebraic Methods Program. 111, 100513 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"31_CR18","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100747","volume":"126","author":"S Eker","year":"2022","unstructured":"Eker, S.: Associative unification in Maude. J. Log. Algebraic Methods Program. 126, 100747 (2022)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"31_CR19","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":"31_CR20","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":"31_CR21","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":"31_CR22","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. Theoret. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"20","key":"31_CR23","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. Log. Program. 19(20), 503\u2013581 (1994)","journal-title":"J. Log. Program."},{"issue":"4","key":"31_CR24","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/36330.36332","volume":"21","author":"D Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P.: Matching, unification and complexity. SIGSAM Bull. 21(4), 6\u20139 (1987)","journal-title":"SIGSAM Bull."},{"key":"31_CR25","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1016\/j.jcss.2018.04.002","volume":"96","author":"S Lucas","year":"2018","unstructured":"Lucas, S., Meseguer, J., Guti\u00e9rrez, R.: The 2D dependency pair framework for conditional rewrite systems. Part I: definition and basic processors. J. Comput. Syst. Sci. 96, 74\u2013106 (2018)","journal-title":"J. Comput. Syst. Sci."},{"issue":"8","key":"31_CR26","doi-asserted-by":"publisher","first-page":"1611","DOI":"10.1007\/s10817-020-09542-3","volume":"64","author":"S Lucas","year":"2020","unstructured":"Lucas, S., Meseguer, J., Guti\u00e9rrez, R.: The 2D dependency pair framework for conditional rewrite systems - Part II: advanced processors and implementation techniques. J. Autom. Reason. 64(8), 1611\u20131662 (2020)","journal-title":"J. Autom. Reason."},{"key":"31_CR27","doi-asserted-by":"crossref","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. Edition, pages 1\u201387. Kluwer Academic Publishers (2002). First published as SRI Technical report SRI-CSL-93-05, August 1993","DOI":"10.1007\/978-94-017-0464-9_1"},{"key":"31_CR28","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":"31_CR29","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":"31_CR30","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":"31_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-662-57669-4_2","volume-title":"Logic, Language, Information, and Computation","author":"J Meseguer","year":"2018","unstructured":"Meseguer, J.: Symbolic reasoning methods in rewriting logic and Maude. In: Moss, L.S., de Queiroz, R., Martinez, M. (eds.) WoLLIC 2018. LNCS, vol. 10944, pp. 25\u201360. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-57669-4_2"},{"key":"31_CR32","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":"31_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-68446-4_1","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J Meseguer","year":"2021","unstructured":"Meseguer, J.: Symbolic computation in Maude: some tapas. In: LOPSTR 2020. LNCS, vol. 12561, pp. 3\u201336. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_1"},{"key":"31_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-030-63595-4_7","volume-title":"Rewriting Logic and Its Applications","author":"J Meseguer","year":"2020","unstructured":"Meseguer, J., Skeirik, S.: Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification. In: Escobar, S., Mart\u00ed-Oliet, N. (eds.) WRLA 2020. LNCS, vol. 12328, pp. 114\u2013135. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63595-4_7"},{"issue":"1\u20132","key":"31_CR35","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 verification of cryptographic protocols. High.-Order Symb. Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"High.-Order Symb. Comput."},{"key":"31_CR36","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 371\u2013443. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"31_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-12904-4_3","volume-title":"Rewriting Logic and Its Applications","author":"PC \u00d6lveczky","year":"2014","unstructured":"\u00d6lveczky, P.C.: Real-time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42\u201379. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_3"},{"issue":"1\u20132","key":"31_CR38","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time Maude. High.-Order Symb. Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"High.-Order Symb. Comput."},{"issue":"2","key":"31_CR39","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"GE Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. Assoc. Comput. Mach. 28(2), 233\u2013264 (1981)","journal-title":"J. Assoc. Comput. Mach."},{"key":"31_CR40","unstructured":"Plotkin, G.: Building-in equational theories. In: Meltzer, B., Michie, D. (eds.) 1971 Proceedings of the Seventh Annual Machine Intelligence Workshop on Machine Intelligence 7, Edinburgh, pp. 73\u201390. Edinburgh University Press (1972)"},{"issue":"1","key":"31_CR41","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(1), 23\u201341 (1965)","journal-title":"J. Assoc. Comput. Mach."},{"key":"31_CR42","unstructured":"Rocha, C., Meseguer, J.: Five isomorphic Boolean theories and four equational decision procedures. Technical report UIUCDCS-R-2007-2818, CS Department, University of Illinois at Urbana-Champaign, February 2007. http:\/\/hdl.handle.net\/2142\/11295"},{"key":"31_CR43","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":"31_CR44","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. Algebr. Meth. Program. 96, 81\u2013110 (2018)","journal-title":"J. Log. Algebr. Meth. Program."},{"issue":"4","key":"31_CR45","doi-asserted-by":"publisher","first-page":"315","DOI":"10.3233\/FI-2020-1926","volume":"173","author":"S Skeirik","year":"2020","unstructured":"Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Fundam. Inform. 173(4), 315\u2013382 (2020)","journal-title":"Fundam. Inform."},{"key":"31_CR46","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"},{"issue":"2","key":"31_CR47","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."},{"issue":"2\u20133","key":"31_CR48","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10703-016-0263-6","volume":"50","author":"Y Zheng","year":"2017","unstructured":"Zheng, Y., et al.: Z3str2: an efficient solver for strings, regular expressions, and length constraints. Formal Methods Syst. Design 50(2\u20133), 249\u2013288 (2017)","journal-title":"Formal Methods Syst. Design"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:15:50Z","timestamp":1659316550000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}