Notions and Notation
Notation and basic definitions in unification theory are well known and have found their way into many and diverse academic fields and most monographs and textbooks on automated reasoning contain sections on unification.
In the following we unify the various presentations of the necessary concepts for unification towards a concise notation which serves our purpose and we show how the additional concepts for essential unification can be built upon these definitions. The notion of an algebra given below embraces algebraic structures and the original notions in computational logic, recursive function theory, theory of automata or automated theorem proving are compatible and natural applications.
Signatures, Terms and Term Algebras
A signature is a finite set F of function symbols with a nonnegative integer n, called arity, that is assigned to each member f of F and f is an n-ary function symbol. The subset of n-ary function symbols in F is denoted by Fn. An algebra of type F is an ordered pair A = (A, F) where A is a nonempty set and F is a family of finitary operations on A indexed by the signature F such that corresponding to each n-ary function symbol f in Fn there is an n-ary operation fA on A. The set A is called the carrier of the algebra A = (A, F).
Let X be a set of (distinct) variables. Let F be a signature. The set T(F, X) of (syntactic) terms of F over X is the smallest set
- (i) comprising X and F0 and
- (ii) if t,...,tn in T (F, X) and f in Fn then f (t, ...,tn) in T (F, X)
The set of variable-free terms are called ground terms. The set of variables occurring in a term t is denoted by Var (t). The set of sub terms of a term f (t, ...,tn) contains the term itself and is closed recursively by containing t,...,tn. It is denoted by Sub(t).
Given F and X,then the termalgebra oftype F over X,denoted by (T (F, X), F), has as its universe the set of terms T (F, X) and the fundamental operations satisfying
for f in Fn and terms t,...,tn in T (F, X). Term algebras give an algebraic structure to (syntactic) terms and focus the attention on Herbrand interpretations, where the set of terms itself is the carrier.