Unification in the empty flat theories with sequence variables and flexible arity symbols

T. Kutsia. Unification in the empty flat theories with sequence variables and flexible arity symbols. pages 20-24, 6, 2001.

Autoren
  • Teimur Kutsia
TypSonstiges
NoteExtended 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
Monat6
Jahr2001
Seiten20-24
Abstract 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.