<div class="csl-bib-body">
<div class="csl-entry">Graczoll, S. (2011). <i>Extending VMTL by a more flexible control and new methods</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-55400</div>
</div>
VMTL (Vienna Modular Termination Laboratory) ist ein Tool zur automatischen Suche von Terminationsbeweisen für Termersetzungssysteme (TRSs). Die Beweissuche in VMTL basiert auf dem Dependency Pair (DP) Framework. Dabei wird das auf Termination zu untersuchende TRS zunächst in das zugehörige sogenannte DP-Problem transformiert, welches dann durch Anwendung von DP-Prozessoren sukzessive vereinfacht wird, bis das Problem (im besten Fall) trivial wird, wodurch dann Termination des ursprünglichen TRS bewiesen ist.<br />Ein Nachteil der DP Methode ist, dass es im Allgemeinen nicht möglich ist, von DP-Pro\-blemen wieder zu den entsprechenden TRSs zurückzukehren. Aus diesem Grund ist es wünschenswert, ein flexibles Framework für Preprocessing zur Verfügung zu haben, um bereits vor der DP-Analyse Vereinfachungen durchführen zu können, die die (Nicht-)Ter\-mi\-nations\-eigenschaften des zu untersuchenden TRS bewahren.<br />\fussy Eines der Ziele dieser Arbeit ist der Entwurf und die Implementierung eines solchen Preprocessing Framework auf Basis klassischer (direkter) Terminationsbeweismethoden.<br />Weiters werden im Zuge dieser Arbeit zwei neue Ansätze für Terminationsbeweismethoden implementiert:<br />Knuth-Bendix Orderings (KBO) sowie Semantic Labeling. Beide Techniken werden sowohl als direkte Methoden wie auch als DP-Prozessoren umgesetzt.<br />Die Beweissuche vieler Methoden und Prozessoren lässt sich effizient als SAT- oder SMT-Problem formulieren.<br />In dieser Arbeit entwickeln wir ein neues SAT/SMT-solving Toolkit, welches innerhalb von VMTL genutzt werden kann, um SAT/SMT-Aufgaben zu formulieren und zu lösen.<br />
de
dc.description.abstract
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.<br />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.<br />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.<br />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.<br />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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
VMTL
de
dc.subject
Termersetzungssysteme
de
dc.subject
Termination
de
dc.subject
Knuth-Bendix Orderings
de
dc.subject
Semantic Labeling
de
dc.subject
Root-Labeling
de
dc.subject
VMTL
en
dc.subject
Term Rewriting Systems
en
dc.subject
Termination
en
dc.subject
Knuth-Bendix Orderings
en
dc.subject
Semantic Labeling
en
dc.subject
Root-Labeling
en
dc.title
Extending VMTL by a more flexible control and new methods