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

Autoren Teimur Kutsia
TitelUnification in the empty flat theories with sequence variables and flexible arity symbols
Typsonst
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
MonatJune
Jahr2001
Seiten20-24
SCCH ID#126
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.