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 Giesl | 1 | 2048 | 124.90 |
René Thiemann | 2 | 984 | 69.38 |
Peter Schneider-kamp | 3 | 985 | 58.56 |
Stephan Falke | 4 | 511 | 27.86 |