Title
Automated Termination Proofs with AProVE
Abstract
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.
Year
DOI
Venue
2004
10.1007/978-3-540-25979-4_15
Lecture Notes in Computer Science
Keywords
Field
DocType
graphical interface
Logic program,Dependency pairs,Programming language,Computer science,Algorithm,Theoretical computer science,Mathematical proof,Graphical user interface,User interface,Dependency graph,Gas meter prover
Conference
Volume
ISSN
Citations 
3091
0302-9743
88
PageRank 
References 
Authors
6.72
24
4
Name
Order
Citations
PageRank
Jürgen Giesl12048124.90
René Thiemann298469.38
Peter Schneider-kamp398558.56
Stephan Falke451127.86