[Zurück]

S. Graczoll:
"Extending VMTL by a More Flexible Control and New Methods";
Betreuer/in(nen): B. Gramlich; Institut fuer Computersprachen, 2011; Abschlussprüfung: 22.11.2011.

VMTL (Vienna Modular Termination Laboratory) is a tool for automated termination proof search for term rewriting systems (TRSs). It is based on the dependency pair (DP) framework.
In this setting an initially given TRS is first transformed into a so-called DP problem which is then successively simplified using DP-processors until (hopefully) the problem becomes trivial,
which means that termination of the initial TRS has been proved.
Once the DP method has been started, it is not possible any more to go back from DP problems to corresponding TRSs. Therefore, it is desirable to have strong and flexible preprocessing
mechanisms at hand that simplify the original TRS as much as possible, in a way such that (non-)termination is preserved, before the DP analysis is started.
In this master´s thesis, we design and implement a preprocessing framework for VMTL, that allows for a modular integration of direct termination proof methods.
Furthermore, two new approaches for proving termination of TRSs are added, namely Knuth-Bendix Orderings (KBO) and Semantic Labeling. Both techniques are incorporated as direct methods and as DP-processors.
In many cases, the proof search of direct methods and DP processors can be modelled efficiently as a SAT or SMT problem. In order to ease the generation and representation of such problems, we develop a new SAT/SMT solving toolkit for use within VMTL.

http://publik.tuwien.ac.at/files/PubDat_206729.pdf