Effectively Checking or Disproving the Finite Variant Property

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 finite set \{t_{1},\ldots,t_{n}\} of \rightarrow_{\Delta,B}-normalized instances of t so that any instance of t normalizes to an instance of some t_{i} 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, both an algorithm ensuring the sufficient condition, and thus FV, and another disproving the necessary condition, and thus disproving FV. These algorithms can check automatically a number of examples and counterexamples of FV known in the literature