First-order unification using variable-free relational algebra *

We present a framework for the representation and resolution of first-order unification problems and their abstract syntax in a variable-free relational formalism which is an executable variant of the Tarski-Givant relation algebra and of Freyd's allegories restricted to the fragment necessary to compile and run logic programs. We develop a decision procedure for validity of relational terms, which corresponds to solving the original unification problem. The decision procedure is carried out by a conditional relational-term rewriting system. There are advantages over classical unification approaches. First, cumbersome and underspecified meta-logical procedures (name clashes, substitution, etc.) and their properties (invariance under substitution of ground terms, equality's congruence with respect to term forming, etc.) are captured algebraically within the framework. Second, other unification problems can be accommodated, for example, existential quantification in the logic can be interpreted as a new operation whose effect is to formalize the costly and error prone handling of fresh names (renaming apart).