References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. D. Kapur & P. Narendran (1987): Matching, Unification and Complexity. ACM SIGSAM Bulletin 21(4), pp. 6–9, doi:10.1145/36330.36332.
  26. 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.
  27. 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.
  28. 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.
  29. 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.
  30. 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.
  31. 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.
  32. 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.
  33. 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.
  34. 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.
  35. 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.
  36. TeReSe (2003): Term Rewriting Systems. Cambridge University Press, doi:10.1017/S095679680400526X.
  37. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org