Deciding knowledge in security protocols under equational theories, Theor. Comput. Sci, vol.367, issue.1-2, pp.2-32, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00000554
Calculs Associatifs-Commutatifs -Etude et réalisation du système UNIFAC, 1991. ,
AC-Unification race: The system solving approach, implementation and benchmarks, J. Symb. Comput, vol.14, issue.1, pp.51-70, 1992. ,
New results on rewrite-based satisfiability procedures, ACM Trans. Comput. Log, vol.10, issue.1, p.51, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00576862
A rewriting approach to satisfiability procedures, Inf. Comput, vol.183, issue.2, pp.140-164, 2003. ,
Combination of compatible reduction orderings that are total on ground terms, Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS-97), pp.2-13, 1997. ,
Combination of constraint solvers for free and quasi-free structures, Theoretical Computer Science, vol.192, pp.107-161, 1998. ,
Combination techniques and decision problems for disunification, Theoretical Computer Science, vol.142, issue.2, pp.229-255, 1995. ,
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Information & Computation, vol.204, issue.10, pp.1413-1452, 2006. ,
, Term rewriting and all that, 1998.
Unification in the union of disjoint equational theories: Combining decision procedures, Journal of Symbolic Computation, vol.21, issue.2, pp.211-243, 1996. ,
Unification theory, Handbook of Automated Reasoning, pp.445-532, 2001. ,
Deciding the word problem in the union of equational theories, Information and Computation, vol.178, issue.2, pp.346-390, 2002. ,
Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput, vol.4, issue.3, pp.217-247, 1994. ,
Basic paramodulation, Inf. Comput, vol.121, issue.2, pp.172-192, 1995. ,
Modeling and verifying security protocols with the Applied Pi calculus and proverif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01423760
A taxonomy of theorem-proving strategies, Artificial Intelligence Today -Recent Trends and Developments, vol.1600, pp.43-84, 1999. ,
ELAN from a rewriting logic point of view, Theor. Comput. Sci, vol.285, issue.2, pp.155-185, 2002. ,
Combining unification algorithms, Journal Symbolic Computation, vol.16, issue.6, pp.597-626, 1993. ,
All About Maude -A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol.4350, 2007. ,
Syntacticness, cycle-syntacticness, and shallow theories, Inf. Comput, vol.111, issue.1, pp.154-191, 1994. ,
The finite variant property: How to get rid of some algebraic properties, Term Rewriting and Applications, 16th International Conference, RTA 2005, vol.3467, pp.294-307, 2005. ,
Combination Techniques for Non-disjoint Equational Theories, Proc. of 12th International Conference on Automated Deduction, vol.814, pp.267-281, 1994. ,
Rule-based unification in combined theories and the finite variant property, Language and Automata Theory and Applications -13th International Conference, vol.11417, pp.356-367, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01988419
Hierarchical combination, Automated Deduction -CADE-24 -24th International Conference on Automated Deduction, vol.7898, pp.249-266, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00878649
Unification and matching in hierarchical combinations of syntactic theories, Frontiers of Combining Systems -10th International Symposium, vol.9322, pp.291-306, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01206669
Notions of knowledge in combinations of theories sharing constructors, Automated Deduction -CADE 26 -26th International Conference on Automated Deduction, vol.10395, pp.60-76, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01587181
Maude-NPA: Cryptographic protocol analysis modulo equational properties, Foundations of Security Analysis and Design V, vol.5705, pp.1-50, 2007. ,
Folding variant narrowing and optimal variant termination, J. Log. Algebr. Program, vol.81, issue.7-8, pp.898-928, 2012. ,
Solving equations in abstract algebras: a rule-based survey of unification, pp.257-321, 1991. ,
Completion of a set of rules modulo a set of equations, SIAM J. Comput, vol.15, issue.4, pp.1155-1194, 1986. ,
Complexity of unification problems with associativecommutative operators, J. Autom. Reasoning, vol.9, issue.2, pp.261-288, 1992. ,
Double-exponential complexity of computing a complete set of AC-unifiers, Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), pp.11-21, 1992. ,
Syntactic theories and unification, Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), pp.270-277, 1990. ,
Rule-based constraint programming, Fundam. Inform, vol.34, issue.3, pp.225-262, 1998. ,
URL : https://hal.archives-ouvertes.fr/inria-00098476
Automated Deduction -CADE-18, 18th International Conference on Automated Deduction, vol.2392, pp.471-485, 2002. ,
The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification -25th International Conference, CAV 2013, vol.8044, pp.696-701, 2013. ,
Variant-based satisfiability in initial algebras, Sci. Comput. Program, vol.154, pp.3-41, 2018. ,
A pattern matching compiler for multiple target languages, Compiler Construction, 12th International Conference, CC 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, vol.2622, pp.61-76, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099427
Simplification by cooperating decision procedures, ACM Transations on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979. ,
Paramodulation-based theorem proving, Handbook of Automated Reasoning, pp.371-443, 2001. ,
Combining matching algorithms: The regular case, Journal of Symbolic Computation, vol.12, issue.6, pp.633-654, 1991. ,
Proof transformations for equational theories, Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), pp.278-288, 1990. ,
E-unification with constants vs. general E-unification, J. Autom. Reasoning, vol.48, issue.3, pp.363-390, 2012. ,
The joint of equational theories, Colloquium Mathematicum, pp.15-25, 1974. ,
Combining Decision Algorithms for Matching in the Union of Disjoint Equational Theories, Information and Computation, vol.126, issue.2, pp.144-160, 1996. ,
Matching with free function symbols -A simple extension of matching?, Rewriting Techniques and Applications, 12th International Conference, RTA, vol.2051, pp.276-290, 2001. ,
URL : https://hal.archives-ouvertes.fr/inria-00108076
Matching in a class of combined non-disjoint theories, 19th International Conference on Automated Deduction, vol.2741, pp.212-227, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099610
Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, vol.8, pp.51-99, 1989. ,
Unification in permutative equational theories is undecidable, J. Symb. Comput, vol.8, issue.4, pp.415-421, 1989. ,
Unification in combinations of collapse-free theories with disjoint sets of function symbols, Proc. of the 8th International Conference on Automated Deduction, vol.230, pp.431-449, 1986. ,
Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures, Theoretical Computer Science, vol.290, issue.1, pp.291-353, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099668
Unification in combinations of collapse-free regular theories, Journal of Symbolic Computation, vol.3, issue.1/2, pp.153-181, 1987. ,