M. Alpuente, S. Escobar & J. Iborra (2009):
Termination of Narrowing Revisited.
Theoretical Computer Science 410(46),
pp. 4608–4625,
doi:10.1016/j.tcs.2009.07.037.
M. Alpuente, S. Escobar & J. Iborra (2011):
Modular Termination of Basic Narrowing and Equational Unification.
Logic Journal of the IGPL 19(6),
pp. 731–762,
doi:10.1007/978-3-540-70590-1_1.
F. Baader & W. Snyder (2001):
Unification Theory.
In: J. A. Robinson & A. Voronkov: Handbook of Automated Reasoning I.
Elsevier Science,
pp. 447–533,
doi:10.1016/B978-044450813-3/50010-2.
K. Bae, S. Escobar & J. Meseguer (2013):
Abstract Logical Model Checking of Infinite-State Systems Using Narrowing.
In: Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
LIPIcs 21.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
pp. 81–96,
doi:10.4230/LIPIcs.RTA.2013.81.
D. Baelde, S. Delaune, I. Gazeau & S. Kremer (2017):
Symbolic Verification of Privacy-Type Properties for Security Protocols with XOR.
In: Proceedings of the 30th International Symposium on Computer Security Foundations (CSF 2017).
IEEE Computer Society Press,
pp. 234–248,
doi:10.1109/CSF.2017.22.
C. Bouchard, K. A. Gero, C. Lynch & P. Narendran (2013):
On Forward Closure and the Finite Variant Property.
In: Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCos 2013),
Lecture Notes in Computer Science 8152.
Springer,
pp. 327–342,
doi:10.1007/978-3-642-40885-4_23.
R. M. Burstall & J. A. Goguen (1982):
Algebras, Theories and Freeness: An Introduction for Computer Scientists.
In: M. Broy & G. Schmidt: Theoretical Foundations of Programming Methodology,
NATO Science Series 91.
Springer,
pp. 329–349,
doi:10.1007/978-94-009-7893-5_11.
A. Cholewa, J. Meseguer & S. Escobar (2014):
Variants of Variants and the Finite Variant Property.
Technical Report.
University of Illinois at Urbana-Champaign.
Available at http://hdl.handle.net/2142/47117.
M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, J. Meseguer, R. Rubio & C. Talcott (2020):
Maude Manual (Version 3.0).
Technical Report.
SRI International Computer Science Laboratory.
Available at: http://maude.cs.uiuc.edu.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer & C. Talcott (2007):
All About Maude: A High-Performance Logical Framework.
Springer,
doi:10.1007/978-3-540-71999-1.
H. Comon-Lundh & S. Delaune (2005):
The Finite Variant Property: How to Get Rid of Some Algebraic Properties.
In: Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005),
Lecture Notes in Computer Science 3467.
Springer,
pp. 294–307,
doi:10.1007/978-3-540-32033-3_22.
J. Dreier, L. Hirschi, S. Radomirovic & R. Sasse (2018):
Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR.
In: Proceedings of the 31st International Symposium on Computer Security Foundations (CSF 2018).
IEEE Computer Society Press,
pp. 359–373,
doi:10.1109/CSF.2018.00033.
F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer, R. Rubio & C. Talcott (2020):
Programming and Symbolic Computation in Maude.
Journal of Logical and Algebraic Methods in Programming 110,
doi:10.1016/j.jlamp.2019.100497.
F. Durán, S. Lucas & J. Meseguer (2009):
Termination Modulo Combinations of Equational Theories.
In: Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCos 2009),
Lecture Notes in Computer Science 5749.
Springer,
pp. 246–262,
doi:10.1007/978-3-642-04222-5_15.
F. Durán & J. Meseguer (2012):
On the Church-Rosser and Coherence Properties of Conditional Order-sorted Rewrite Theories.
The Journal of Logic and Algebraic Programming 81(7–8),
pp. 816–850,
doi:10.1016/j.jlap.2011.12.004.
F. Durán, J. Meseguer & C. Rocha (2020):
Ground Confluence of Order-Sorted Conditional Specifications Modulo Axioms.
Journal of Logical and Algebraic Methods in Programming 111,
pp. 100513,
doi:10.1016/jj.jlamp.2019.100513.
A. K. Eeralla, S. Erbatur, A. M. Marshal & C. Ringeissen (2019):
Rule-based Unification in Combined Theories and the Finite Variant Property.
In: Proceedings of the 13th International Conference on Language and Automata Theory and Applications (LATA 2019),
Lecture Notes in Computer Science 11417.
Springer,
pp. 356–367,
doi:10.1007/978-3-030-13435-8_26.
S. Erbatur, D. Kapur, A. M. Marshall, P. Narendran & C. Ringeissen (2015):
Unification and Matching in Hierarchical Combinations of Syntactic Theories.
In: Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCos 2015),
Lecture Notes in Computer Science 9322.
Springer,
pp. 291–306,
doi:10.1007/978-3-319-24246-0_18.
S. Escobar, C. Meadows & J. Meseguer (2009):
Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties.
In: Foundations of Security Analysis and Design V (FOSAD 2007/2008/2009 Tutorial Lectures),
Lecture Notes in Computer Science 5705.
Springer,
pp. 1–50,
doi:10.1007/978-3-642-03829-7_1.
S. Escobar & J. Meseguer (2007):
Symbolic Model Checking of Infinite-State Systems Using Narrowing.
In: Proceedings of the 18th International Conference on Term Rewriting and Applications (RTA 2007),
Lecture Notes in Computer Science 4533.
Springer,
pp. 153–168,
doi:10.1007/978-3-540-73449-9_13.
S. Escobar & J. Sapiña (2019):
Most General Variant Unifiers.
In: Proceedings of the 35th International Conference on Logic Programming (ICLP 2019) - Technical Communications,
Electronic Proceedings in Theoretical Computer Science 306.
Open Publishing Association,
pp. 154–167,
doi:10.4204/EPTCS.306.21.
S. Escobar, R. Sasse & J. Meseguer (2012):
Folding Variant Narrowing and Optimal Variant Termination.
The Journal of Logic and Algebraic Programming 81(7–8),
pp. 898–928,
doi:10.1016/j.jlap.2012.01.002.
J. P. Jouannaud, C. Kirchner & H. Kirchner (1983):
Incremental Construction of Unification Algorithms in Equational Theories.
In: Proceedings of the 17th International Colloquium on Automata, Languages and Programming (ICALP 1990),
Lecture Notes in Computer Science 154.
Springer,
pp. 361–373,
doi:10.1007/BFb0036921.
J. P. Jouannaud & H. Kirchner (1986):
Completion of a Set of Rules Modulo a Set of Equations.
SIAM Journal on Computing 15(4),
pp. 1155–1194,
doi:10.1137/0215084.
D. Kapur & P. Narendran (1987):
Matching, Unification and Complexity.
ACM SIGSAM Bulletin 21(4),
pp. 6–9,
doi:10.1145/36330.36332.
S. Lucas & J. Meseguer (2016):
Normal Forms and Normal Theories in Conditional Rewriting.
Journal of Logical and Algebraic Methods in Programming 85,
pp. 67–97,
doi:10.1016/j.jlamp.2015.06.001.
J. Meseguer (1992):
Conditional Rewriting Logic as a United Model of Concurrency.
Theoretical Computer Science 96(1),
pp. 73–155,
doi:10.1016/0304-3975(92)90182-F.
J. Meseguer (1997):
Membership Algebra as a Logical Framework for Equational Specification.
In: Proceedings of the 12th International Workshop on Algebraic Development Techniques (WADT 1997),
Lecture Notes in Computer Science 1376.
Springer,
pp. 18–61,
doi:10.1007/3-540-64299-4_26.
J. Meseguer (2012):
Twenty Years of Rewriting Logic.
The Journal of Logic and Algebraic Programming 81(7-8),
pp. 721–781,
doi:10.1016/j.jlap.2012.06.003.
J. Meseguer (2017):
Strict Coherence of Conditional Rewriting Modulo Axioms.
Theoretical Computer Science 672,
pp. 1–35,
doi:10.1016/j.tcs.2016.12.026.
J. Meseguer (2018):
Symbolic Reasoning Methods in Rewriting Logic and Maude.
In: Proceedings of the 25th International Workshop on Logic, Language, Information, and Computation (WoLLIC 2018),
Lecture Notes in Computer Science 10944.
Springer,
pp. 25–60,
doi:10.1007/978-3-662-57669-4_2.
J. Meseguer (2018):
Variant-based Satisfiability in Initial Algebras.
Science of Computer Programming 154,
pp. 3–41,
doi:10.1016/j.scico.2017.09.001.
J. Meseguer (2020):
Generalized Rewrite Theories, Coherence Completion, and Symbolic Methods.
Journal of Logical and Algebraic Methods in Programming 110,
doi:10.1016/j.jlamp.2019.100483.
A. Riesco (2014):
Using Big-Step and Small-Step Semantics in Maude to Perform Declarative Debugging.
In: Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014),
Lecture Notes in Computer Science 8475.
Springer,
pp. 52–68,
doi:10.1007/978-3-319-07151-0_4.
V. Rusu (2010):
Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications.
In: Proceedings of the 4th International Conference on Tests and Proofs (TAP 2010),
Lecture Notes in Computer Science 6143.
Springer,
pp. 135–150,
doi:10.1007/978-3-642-13977-2_12.
E. Tushkanova, A. Giorgetti, C. Ringeissen & O. Kouchnarenko (2015):
A Rule-based System for Automatic Decidability and Combinability.
Science of Computer Programming 99,
pp. 3–23,
doi:10.1016/j.scico.2014.02.005.