Automated termination proofs with AProVE

Jürgen Giesl*, René Thiemann, Peter Schneider-Kamp, Stephan Falke

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review


We describe the system ProVE, an automated prover to verify (innermost) termination of term rewrite systems (TRSs). For this system, we have developed and implemented efficient algorithms based on classical simplification orders, dependency pairs, and the size-change principle. In particular, it contains many new improvements of the dependency pair approach that make automated termination proving more powerful and efficient. In ProVE, termination proofs can be performed with a user-friendly graphical interface and the system is currently among the most powerful termination provers available.

Original languageEnglish
Book seriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages (from-to)210-220
Number of pages11
Publication statusPublished - 1. Dec 2004


Cite this