Technical report Frank / JohannWolfgangGoetheUniversität, Fachbereich Informatik und Mathematik, Institut für Informatik
2 search hits
 2

An algorithm for distributive unification
(1994)

Manfred SchmidtSchauß
 We consider unification of terms under the equational theory of twosided distributivity D with the axioms x*(y+z) = x*y + x*z and (x+y)*z = x*z + y*z. The main result of this paper is that Dunification is decidable by giving a nondeterministic transformation algorithm. The generated unification are: an AC1problem with linear constant restrictions and a secondorder unification problem that can be transformed into a wordunification problem that can be decided using Makanin's algorithm. This solves an open problem in the field of unification. Furthermore it is shown that the wordproblem can be decided in polynomial time, hence Dmatching is NPcomplete.
 1

Unification of stratified secondorder terms
(1994)

Manfred SchmidtSchauß
 We consider the problem of unifying a set of equations between secondorder terms. Terms are constructed from function symbols, constant symbols and variables, and furthermore using monadic secondorder variables that may stand for a term with one hole, and parametric terms. We consider stratified systems, where for every firstorder and secondorder variable, the string of secondorder variables on the path from the root of a term to every occurrence of this variable is always the same. It is shown that unification of stratified secondorder terms is decidable by describing a nondeterministic decision algorithm that eventually uses Makanin's algorithm for deciding the unifiability of word equations. As a generalization, we show that the method can be used as a unification procedure for nonstratified secondorder systems, and describe conditions for termination in the general case.