=ADD=
=reftype=
14
=number=
02-09
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2002/02-09.ps.gz
=year=
2002
=month=
05
=author=
Kutsia; Teimuraz
=title=
Solving and Proving in Equational Theories with Sequence Variables and Flexible Arity Symbols
=abstract=
We study equational theories whose alphabet includes
individual and sequence variables, constants and fixed and
flexible arity function symbols. Sequence variables are variables
which can be instantiated by an arbitrary finite (possibly empty)
sequence of terms. Flexible arity function symbols can take
arbitrary finite (possibly empty) sequence of arguments. In this
thesis we

- describe a Birkhoff-style calculus for pure equational logic
with sequence variables and flexible arity symbols and prove its
soundness and completeness;

- design unification procedures for free, flat, restricted flat
and orderless equational theories with sequence variables and flexible
arity symbols, prove decidability of the unification problem in these
theories and minimality and completeness of the unification procedures;

- design a minimal and complete unification procedure for an extension
of the free theory with patterns;

- define ground total reduction orderings for terms and pattern-terms
with sequence variables and flexible arity symbols;

- show that the basic equational superposition with ordering and
equational constraints is a refutationally complete proving method
for the free theory with sequence variables and flexible arity symbols;

- show that for a special class of equations in the free theory with
sequence variables and flexible arity symbols, unfailing completion
can be used as a refutationally complete proving method.

The unification procedure for the free theory is implemented in
the mathematical software system Theorema.
=note=
PhD Thesis
=sponsor=
FWF project SFB F1302 (Theorema), SCCH projects MathSoft and ForMI
=keywords=
unification, superposition, automated theorem proving, equational reasoning