# Browse Dept. of Computer Science by Author "Escobar, Santiago"

• (2014-08-29)
For an unconditional equational theory (Σ,E) whose oriented equations E⃗ are confluent and terminating, narrowing provides an E-unification algorithm. This has been generalized by various authors in two directions: (i) by ...

application/pdf

PDF (589kB)
• (2008-04)
An equational theory decomposed into a set B of equational axioms and a set \Delta of rewrite rules has the \emph{finite variant} (FV) \emph{property} in the sense of Comon-Lundh and Delaune iff for each term t there is a ...

application/pdf

PDF (468kB)
• (Elsevier, 2012)
Automated reasoning modulo an equational theory $\caE$ is a fundamental technique in many applications. If $\caE$ can be split as a disjoint union $E\!\cup \!Ax$ in such a way that $E$ is confluent, terminating, ...

application/pdf

PDF (443kB)
• (2011-07-28)
Generalization, also called anti-unification, is the dual of unification. Given terms t and t', a generalization is a term t'' of which t and t' are substitution instances. The dual of a most general unifier (mgu) is that ...

application/pdf

PDF (696kB)
• (2016-07)
Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in ...

application/pdf

PDF (457kB)
• (2007-02)
Rewriting is a general and expressive way of specifying concurrent systems, where concurrent transitions are axiomatized by rewrite rules. Narrowing is a complete symbolic method for model checking reachability properties. ...

application/pdf

PDF (373kB)
• (2007-10)
Narrowing is a well-known complete procedure for equational E-unification when E can be decomposed as a union E = \Delta \uplus B with B a set of axioms for which a finitary unification algorithm exists, and \Delta a set ...

application/pdf

PDF (309kB)
• (2009-03)
For narrowing with a set of rules \Delta modulo a set of axioms B almost nothing is known about terminating narrowing strategies, and basic narrowing is known to be incomplete for B=AC. In this work we ask and answer the ...

application/pdf

PDF (312kB)
• (2009-03)
For narrowing with a set of rules \Delta modulo a set of axioms B almost nothing is known about terminating narrowing strategies, and basic narrowing is known to be incomplete for B=AC. In this work we ask and answer the ...

application/pdf

PDF (312kB)
• (2014-02-11)
Variants and the finite variant property were originally introduced about a decade ago by Hurbert Comon-Lundh and Stephanie Delaune to reason about equational theories that commonly appear in cryptographic protocol analysis. ...

application/pdf

PDF (340kB)