Unification for quantified formulae

Abstract: "Unification for a first order language is a method that attempts to make terms of the language -- via appropriate substitutions -- syntactically identical. The method can be applied directly to quantifier-free formulae and, in this paper, will be extended in a naturaland straightforward way to quantified formulae. The main issue is the treatment of bound variables. Our method is based on a canonical renaming of the bound variables occuring in the input formulae, so that every binding is associated in a special way with a distinct variable. Then, unification works as usual by treating logical connectives like functors and bound variables like constants. Our work is meant to help limit the search of theorem proving algorithms, in particular of those that search directly for natural deduction proofs.