Unification for quantified formulae
journal contributionposted on 01.01.1993 by Sieg, Barbara Kauffmann
Any type of content formally published in an academic journal, usually following a peer-review process.
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."