Title: Extending VMTL by a more flexible control and new methods
Language: English
Authors: Graczoll, Sebastian 
Qualification level: Diploma
Keywords: VMTL; Termersetzungssysteme; Termination; Knuth-Bendix Orderings; Semantic Labeling; Root-Labeling
VMTL; Term Rewriting Systems; Termination; Knuth-Bendix Orderings; Semantic Labeling; Root-Labeling
Advisor: Gramlich, Bernhard
Issue Date: 2011
Number of Pages: 156
Qualification level: Diploma
Abstract: 
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.
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.
\fussy Eines der Ziele dieser Arbeit ist der Entwurf und die Implementierung eines solchen Preprocessing Framework auf Basis klassischer (direkter) Terminationsbeweismethoden.
Weiters werden im Zuge dieser Arbeit zwei neue Ansätze für Terminationsbeweismethoden implementiert:
Knuth-Bendix Orderings (KBO) sowie Semantic Labeling. Beide Techniken werden sowohl als direkte Methoden wie auch als DP-Prozessoren umgesetzt.
Die Beweissuche vieler Methoden und Prozessoren lässt sich effizient als SAT- oder SMT-Problem formulieren.
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.

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.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-55400
http://hdl.handle.net/20.500.12708/10626
Library ID: AC07812001
Organisation: E185 - Institut für Computersprachen 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

File Description SizeFormat
Extending VMTL by a more flexible control and new methods.pdf1.23 MBAdobe PDFThumbnail
 View/Open
Show full item record

Page view(s)

9
checked on Feb 18, 2021

Download(s)

47
checked on Feb 18, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.