An equational theory decomposed into a set B of equational axioms and a set Δ of rewrite rules has the finite variant (FV) property in the sense of Comon-Lundh and Delaune iff for each term t there is a finite set {t 1,..., tn} of → Δ,B -normalized instances of t so that any instance of t normalizes to an instance of some ti modulo B. This is a very useful property for cryptographic protocol analysis, and for solving both unification and disunification problems. Yet, at present the property has to be established by hand, giving a separate mathematical proof for each given theory: no checking algorithms seem to be known. In this paper we give both a necessary and a sufficient condition for FV from which we derive an algorithm ensuring the sufficient condition, and thus FV. This algorithm can check automatically a number of examples of FV known in the literature. © 2008 Springer-Verlag.
CITATION STYLE
Escobar, S., Meseguer, J., & Sasse, R. (2008). Effectively checking the finite variant property. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5117 LNCS, pp. 79–93). https://doi.org/10.1007/978-3-540-70590-1_6
Mendeley helps you to discover research relevant for your work.