Diploma Thesis Quanti¯er Elimination-based Parametric Solving in Term Algebras

hello Quanti¯er elimination refers to the process of transforming a ¯rst-order formula ' into a quanti¯er-free formula '0 so that ' and '0 are equivalent w.r.t. the un-derlying structure. On the basis of [SW02], we present a quanti¯er elimination procedure for term algebras over suitably expanded ¯nite ¯rst-order languages. The procedure, together with some extensions for increasing its e±ciency, is im-plemented within the logic package Redlog, which is part of the computer algebra system Reduce. The elimination technique used here was introduced by Weispfenning in 1988 and works by substitution of ¯nitely many test terms for the quanti¯ed variables (cf. [Wei88]). The main advantage of this method is its practicability for highly parametric problems. Furthermore, it o®ers a straightforward extension to quan-ti¯er elimination with answers for an outermost existential quanti¯er block. Due to the fact that the ¯rst-order theory of term algebras T does not admi