  Unification and generalization are operations on two terms computing
respectively their greatest lower bound and least upper bound when the terms
are quasi-ordered by subsumption up to variable renaming (i.e., $t_1\preceq
t_2$ iff $t_1 = t_2\sigma$ for some variable substitution $\sigma$). When term
signatures are such that distinct functor symbols may be related with a fuzzy
equivalence (called a similarity), these operations can be formally extended to
tolerate mismatches on functor names and/or arity or argument order. We
reformulate and extend previous work with a declarative approach defining
unification and generalization as sets of axioms and rules forming a complete
constraint-normalization proof system. These include the Reynolds-Plotkin
term-generalization procedures, Maria Sessa's "weak" unification with partially
fuzzy signatures and its corresponding generalization, as well as novel
extensions of such operations to fully fuzzy signatures (i.e., similar functors
with possibly different arities). One advantage of this approach is that it
requires no modification of the conventional data structures for terms and
substitutions. This and the fact that these declarative specifications are
efficiently executable conditional Horn-clauses offers great practical
potential for fuzzy information-handling applications.
