Solving and proving in equational theories with sequence variables and flexible arity symbols

Autoren Teimur Kutsia
TitelSolving and proving in equational theories with sequence variables and flexible arity symbols
TypDissertation
OrtLinz, Austria
UniversitätJohannes Kepler University
MonatMay
Jahr2002
SCCH ID#261
Abstract

We study equational theories whose alphabet includes individual and sequence variables, constants and fixed and flexible arity function symbols and • 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 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 refutation 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 refutation complete proving method. The unification procedure for the free theory is implemented in the mathematical software system Theorema.