{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:02:25Z","timestamp":1762459345596,"version":"3.41.0"},"publisher-location":"Cham","reference-count":84,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319295091"},{"type":"electronic","value":"9783319295107"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-29510-7_1","type":"book-chapter","created":{"date-parts":[[2016,1,29]],"date-time":"2016-01-29T14:39:16Z","timestamp":1454078356000},"page":"3-34","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Variant-Based Satisfiability in Initial Algebras"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,30]]},"reference":[{"issue":"46","key":"1_CR1","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":"1_CR2","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"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Aoto, T., Stratulat, S.: Decision procedures for proving inductive theorems without induction. In: Proceedings of PPDP2014, pp. 237\u2013248. ACM (2014)","DOI":"10.1145\/2643135.2643156"},{"issue":"1","key":"1_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1459010.1459014","volume":"10","author":"Alessandro 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) (2009)","journal-title":"ACM Transactions on Computational Logic"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","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, vol. 1809, pp. 97\u2013108. Springer, Heidelberg (2000)"},{"issue":"2","key":"1_CR6","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":"1_CR7","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 - CADE-18","author":"G Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P.G., Cimatti, A., Kornilowicz, 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)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F Baader","year":"1996","unstructured":"Baader, F., Schulz, K.: Unification in the union of disjoint equational theories: combining decision procedures. J. Symbolic Comput. 21, 211\u2013243 (1996)","journal-title":"J. Symbolic Comput."},{"issue":"2","key":"1_CR9","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0304-3975(94)00277-0","volume":"142","author":"F Baader","year":"1995","unstructured":"Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theor. Comput. Sci. 142(2), 229\u2013255 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/3-540-45406-3_3","volume-title":"Constraints in Computational Logics","author":"F Baader","year":"2001","unstructured":"Baader, F., Schulz, K.U.: Combining constraint solving. In: Comon, H., March\u00e9, C., Treinen, R. (eds.) CCL 1999. LNCS, vol. 2002, pp. 104\u2013158. Springer, Heidelberg (2001)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"1_CR12","doi-asserted-by":"crossref","first-page":"21","DOI":"10.3233\/SAT190028","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. J. Satisfiability Boolean Model. Comput. 3, 21\u201346 (2007)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E., Henzinger, T., Veith, H. (eds.) Handbook of Model Checking. Springer (2017, to appear)","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"1_CR14","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)"},{"issue":"1","key":"1_CR15","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"DA Basin","year":"2001","unstructured":"Basin, D.A., Ganzinger, H.: Automated complexity analysis based on ordered resolution. J. ACM 48(1), 70\u2013109 (2001)","journal-title":"J. ACM"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: Proceedings of 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning. SMT 2008\/BPR 2008, pp. 1\u20135. ACM (2008)","DOI":"10.1145\/1512464.1512466"},{"issue":"1","key":"1_CR17","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}}$$ -satisfiability procedures. J. Log. Comput. 18(1), 77\u201396 (2008)","journal-title":"J. Log. Comput."},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-40885-4_23","volume-title":"Frontiers of Combining Systems","author":"C Lynch","year":"2013","unstructured":"Lynch, C., Gero, K.A., Narendran, P., Bouchard, C.: On forward closure and the finite variant property. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 327\u2013342. Springer, Heidelberg (2013)"},{"issue":"6","key":"1_CR19","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1006\/jsco.1993.1066","volume":"16","author":"A Boudet","year":"1993","unstructured":"Boudet, A.: Combining unification algorithms. J. Symb. Comput. 16(6), 597\u2013626 (1993)","journal-title":"J. Symb. Comput."},{"key":"1_CR20","volume-title":"The Calculus of Computation - Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"RE Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"1_CR22","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., Kremer, S., Ciob\u00e2c\u0103, \u015e.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 108\u2013127. Springer, Heidelberg (2012)"},{"key":"1_CR23","unstructured":"Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, CS Department University of Illinois at Urbana-Champaign, February 2014. http:\/\/hdl.handle.net\/2142\/47117"},{"key":"1_CR24","unstructured":"Ciobaca, S.: Verification of composition of security protocols with applications to electronic voting. Ph.D. thesis, ENS Cachan (2011)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"1_CR26","volume-title":"Set Theory and the Continuum Hypothesis","author":"P Cohen","year":"1966","unstructured":"Cohen, P.: Set Theory and the Continuum Hypothesis. W.A. Benjamin, New York (1966)"},{"key":"1_CR27","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 . 12th October 2007"},{"key":"1_CR28","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. J. Symbolic Comput. 7, 371\u2013425 (1989)","journal-title":"J. Symbolic Comput."},{"issue":"2","key":"1_CR29","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0304-3975(93)90108-6","volume":"118","author":"H Comon","year":"1993","unstructured":"Comon, H.: Complete axiomatizations of some quotient term algebras. Theor. Comput. Sci. 118(2), 167\u2013191 (1993)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"1_CR30","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H Comon","year":"1994","unstructured":"Comon, H., Delor, C.: Equational formulae with membership constraints. Inf. Comput. 112(2), 167\u2013216 (1994)","journal-title":"Inf. Comput."},{"key":"1_CR31","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":"S Delaune","year":"2005","unstructured":"Delaune, S., Comon-Lundh, H.: 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)"},{"key":"1_CR32","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320. North-Holland, Amsterdam (1990)"},{"issue":"3","key":"1_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1352582.1352583","volume":"9","author":"Agostino Dovier","year":"2008","unstructured":"Dovier, A., Piazza, C., Rossi, G.: A uniform approach to constraint-solving for lists, multisets, compact lists, and sets. ACM Trans. Comput. Log. 9(3) (2008)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2\u20133","key":"1_CR34","doi-asserted-by":"crossref","first-page":"201","DOI":"10.3233\/FI-1998-36235","volume":"36","author":"A Dovier","year":"1998","unstructured":"Dovier, A., Policriti, A., Rossi, G.: A uniform axiomatic view of lists, multisets, and sets, and the relevant unification algorithms. Fundam. Inf. 36(2\u20133), 201\u2013234 (1998)","journal-title":"Fundam. Inf."},{"key":"1_CR35","unstructured":"Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Adding Decision Procedures to SMT Solvers using Axioms with Triggers. Journal of Automated Reasoning (2016) (accepted for publication). https:\/\/hal.archives-ouvertes.fr\/hal-01221066"},{"issue":"3","key":"1_CR36","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. Reasoning 48(3), 293\u2013362 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specification 1","author":"H Ehrig","year":"1985","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1. Springer, Heidelberg (1985)"},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-24933-4_15","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"S Eker","year":"2011","unstructured":"Eker, S.: Fast sort computations for order-sorted matching and unification. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 299\u2013314. Springer, Heidelberg (2011)"},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-38574-2_16","volume-title":"Automated Deduction \u2013 CADE-24","author":"CA Lynch","year":"2013","unstructured":"Lynch, C.A., Narendran, P., Escobar, S., Meseguer, J., Liu, Z., Santiago, S., Kapur, D., Sasse, R., Meadows, C., Erbatur, S.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 231\u2013248. Springer, Heidelberg (2013)"},{"key":"1_CR40","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\/2008\/2009 Tutorial Lectures. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009)"},{"key":"1_CR41","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)"},{"key":"1_CR42","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":"1_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-31365-3_20","volume-title":"Automated Reasoning","author":"S Falke","year":"2012","unstructured":"Falke, S., Kapur, D.: Rewriting induction + Linear arithmetic = Decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 241\u2013255. Springer, Heidelberg (2012)"},{"key":"1_CR44","unstructured":"Fay, M.: First-order unification in an equational theory. In: Proceedings of the 4th Workshop on Automated Deduction, pp. 161\u2013167 (1979)"},{"key":"1_CR45","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\u00df, 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)"},{"key":"1_CR46","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)"},{"issue":"2-3","key":"1_CR47","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"Jean H. Gallier","year":"1989","unstructured":"Gallier, J.H., Snyder, W.: Complete sets of transformations for general E-unification. Theor. Comput. Sci. 67(2\u20133), 203\u2013260 (1989). http:\/\/dx.doi.org\/10.1016\/0304-3975(89)90004--2","journal-title":"Theoretical Computer Science"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45744-5_41","volume-title":"Automated Reasoning","author":"J Giesl","year":"2001","unstructured":"Giesl, J., Kapur, D.: Decidable classes of inductive theorems. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 469\u2013484. Springer, Heidelberg (2001)"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-45085-6_3","volume-title":"Automated Deduction \u2013 CADE-19","author":"J Giesl","year":"2003","unstructured":"Giesl, J., Kapur, D.: Deciding inductive validity of equations. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 17\u201331. Springer, Heidelberg (2003)"},{"issue":"1","key":"1_CR50","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95\u2013146 (1992)","journal-title":"J. ACM"},{"key":"1_CR51","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. Theor. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR52","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"TAPSOFT\u201987","author":"J Goguen","year":"1987","unstructured":"Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT\u201987. LNCS, vol. 250, pp. 1\u201322. Springer, Heidelberg (1987)"},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-319-12904-4","volume-title":"Security Standardisation Research","author":"S Escobar","year":"2014","unstructured":"Escobar, S., Meseguer, J., Santiago, S., Meadows, C., Gonz\u00e1lez-Burgue\u00f1o, A.: 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, Heidelberg (2014)"},{"key":"1_CR54","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2012.09.008","volume":"464","author":"B Gramlich","year":"2012","unstructured":"Gramlich, B.: Modularity in term rewriting revisited. Theor. Comput. Sci. 464, 3\u201319 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-32033-3_13","volume-title":"Term Rewriting and Applications","author":"J Hendrix","year":"2005","unstructured":"Hendrix, J., Meseguer, J., Clavel, M.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165\u2013174. Springer, Heidelberg (2005)"},{"key":"1_CR56","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 Meseguer","year":"2006","unstructured":"Meseguer, J., Ohsaki, H., Hendrix, J.: 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)"},{"key":"1_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"JM Hullot","year":"1980","unstructured":"Hullot, J.M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) 5th Conference on Automated Deduction. LNCS, vol. 87, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"key":"1_CR58","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":"JP Jouannaud","year":"1983","unstructured":"Jouannaud, J.P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Diaz, J. (ed.) Automata, Languages and Programming. LNCS, vol. 154, pp. 361\u2013373. Springer, Heidelberg (1983)"},{"key":"1_CR59","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":"2","key":"1_CR60","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BF00245463","volume":"9","author":"D Kapur","year":"1992","unstructured":"Kapur, D., Narendran, P.: Complexity of unification problems with associative-commutative operators. J. Autom. Reasoning 9(2), 261\u2013288 (1992)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR61","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":"C Ringeissen","year":"2005","unstructured":"Ringeissen, C., Tran, D.-K., Ranise, S., Kirchner, H.: 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)"},{"key":"1_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-540-71209-1_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A., Tinelli, C., Grundy, J.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 602\u2013617. Springer, Heidelberg (2007)"},{"key":"1_CR63","doi-asserted-by":"crossref","unstructured":"Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of LICS 2002, p. 7. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029813"},{"key":"1_CR64","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":"D-K Tran","year":"2007","unstructured":"Tran, D.-K., Lynch, C.: Automatic decidability and combinability revisited. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 328\u2013344. Springer, Heidelberg (2007)"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proceedings of LICS 1988, pp. 348\u2013357. IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5132"},{"key":"1_CR66","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: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"1_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-04164-8_4","volume-title":"Semantics and Algebraic Specification","author":"J Meseguer","year":"2009","unstructured":"Meseguer, J.: Order-sorted parameterization and induction. In: Palsberg, J. (ed.) Semantics and Algebraic Specification. LNCS, vol. 5700, pp. 43\u201380. Springer, Heidelberg (2009)"},{"key":"1_CR68","unstructured":"Meseguer, J.: Strict coherence of conditional rewriting modulo axioms. Technical report, C.S. Department, University of Illinois at Urbana-Champaign, August 2014. http:\/\/hdl.handle.net\/2142\/50288"},{"key":"1_CR69","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. Technical report, University of Illinois at Urbana-Champaign, November 2015. http:\/\/hdl.handle.net\/2142\/88408"},{"issue":"1","key":"1_CR70","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1006\/inco.1993.1016","volume":"103","author":"J Meseguer","year":"1993","unstructured":"Meseguer, J., Goguen, J.: Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. Inf. Comput. 103(1), 114\u2013158 (1993)","journal-title":"Inf. Comput."},{"key":"1_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-319-27436-2_3","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J Meseguer","year":"2015","unstructured":"Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. In: Falaschi, M., et al. (eds.) LOPSTR 2015. LNCS, vol. 9527, pp. 36\u201353. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-27436-2_3"},{"key":"1_CR72","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":"2","key":"1_CR73","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":"2","key":"1_CR74","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"issue":"6","key":"1_CR75","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":"1_CR76","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291\u2013302 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR77","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 CSF 2012, pp. 78\u201394. IEEE (2012)","DOI":"10.1109\/CSF.2012.25"},{"issue":"1","key":"1_CR78","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":"4","key":"1_CR79","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"},{"key":"1_CR80","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, Basel (1991)"},{"key":"1_CR81","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: Proceedings of LICS 2001, pp. 29\u201337. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"1_CR82","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-540-30227-8_53","volume-title":"Logics in Artificial Intelligence","author":"C Tinelli","year":"2004","unstructured":"Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 641\u2013653. Springer, Heidelberg (2004)"},{"issue":"3","key":"1_CR83","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y Toyama","year":"1987","unstructured":"Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett. 25(3), 141\u2013143 (1987)","journal-title":"Inf. Process. Lett."},{"key":"1_CR84","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 PPDP 2014, pp. 123\u2013133. ACM (2014)","DOI":"10.1145\/2643135.2643154"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29510-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T07:59:09Z","timestamp":1748764749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29510-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319295091","9783319295107"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29510-7_1","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"30 January 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}