Unification in the empty flat theories with sequence variables and flexible arity symbols
|Titel||Unification in the empty flat theories with sequence variables and flexible arity symbols|
|Note||Extended Abstract published in F.Baader, V.Diekert, C.Tinelli, R.Treinen (eds.), Proceedings of the 15th International Workshop on Unification Siena, Italy, June 18-19, 2001 pp. 20-24|
We define equational theory with sequence variables and flexible arity symbols and consider a general unification problem in two such theories: in an empty theory and in a flat theory (a theory with a flat flexible arity symbol). We prove that unifiability in both theories is decidable and describe unification procedures, which enumerate the minimal and complete set of solutions of the problem and terminate, if the set is finite.