In his framework, subsort declarations are propagated to complex type expressions. As a programming example, a parametric sort "list"("X") may be declared (with "X" being a type parameter as in a C++ template), and from a subsort declaration "int" ⊆ "float" the relation "list"("int") ⊆ "list"("float") is automatically inferred, meaning that each list of integers is also a list of floats. Schmidt-Schauß generalized order-sorted logic to allow for term declarations. As an example, assuming subsort declarations "even" ⊆ "int" and "odd" ⊆ "int", a term declaration like ∀ "i" : "int". ("i" + "i") : "even" allows to declare a property of integer addition that could not be expressed by ordinary overloading. Background on infinite trees:  Unification algorithm, Prolog II:  Applications:  E-unification is the problem of finding solutions to a given set of equations, taking into account some equational background knowledge "E". The latter is given as a set of universal equalities. For some particular sets "E", equation solving algorithms (a.k.a. "E-unification algorithms") have been devised; for others it has been proven that no such algorithms can exist. For example, if and are distinct constants, the equation has no solution with respect to purely syntactic unification, where nothing is known about the operator . However, if the is known to be commutative, then the substitution solves the above equation, since The background knowledge "E" could state the commutativity of by the universal equality " for all ". It is said that "unification is decidable" for a theory, if a unification algorithm has been devised for it that terminates for "any" input problem. It is said that "unification is semi-decidable" for a theory, if a unification algorithm has been devised for it that terminates for any "solvable" input problem, but may keep searching forever for solutions of an unsolvable input problem. Unification is decidable for the following theories:  Unification is semi-decidable for the following theories:  If there is a convergent term rewriting system "R" available for "E", the one-sided paramodulation algorithm can be used to enumerate all solutions of given equations. Starting with "G" being the unification problem to be solved and "S" being the identity substitution, rules are applied nondeterministically until the empty set appears as the actual "G", in which case the actual "S" is a unifying substitution.