Talks and Poster Presentations (with Proceedings-Entry):
F. Schernhammer, B. Gramlich:
"On Some Implementation Aspects of VMTL";
Talk: 10th International Workshop on Termination (WST 2009),
- 2009-06-05; in: "Proc. 10th International Workshop on Termination (WST 2009)",
A. Geser, J. Waldmann (ed.);
VMTL (Vienna Modular Termination Laboratory) is a program designed to (semi-) automatically prove termination of various classes of term rewriting systems, including conditional and context-sensitive ones. VMTL is extensible in that it provides easy to use, public interfaces for the addition of new dependency pair processors and transformations. Moreover, VMTL provides implementations of several standard processors and transformations out of the box. In this work we describe and discuss implementation details of several DP processors currently available in VMTL. In particular the dependency graph, subterm principle, narrowing and instantiation processors are described and several non-standard modifications and generalizations of these processors are proposed.
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.