Name
Abstract | ||
|---|---|---|
In this paper the Recursive Path Ordering is adapted for proving termination of rewriting incrementally. The new ordering, called Recursive Path Ordering with Modules, has as ingredients not only a precedence but also an underlying ordering $\sqsupset_{B}$. It can be used for incremental (innermost) termination proofs of hierarchical unions by defining $\sqsupset_{B}$as an extension of the termination proof obtained for the base system. Furthermore, there are practical situations in which such proofs can be done modularly. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11591191_17 | LPAR |
Keywords | Field | DocType |
practical situation,recursive path ordering,termination proof,hierarchical union,base system | Path-ordering,Discrete mathematics,Computer science,Automated theorem proving,Algorithm,Mathematical proof,Rewriting,Recursion | Conference |
Volume | ISSN | ISBN |
3835 | 0302-9743 | 3-540-30553-X |
Citations | PageRank | References |
1 | 0.39 | 15 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mirtha-Lina Fernández | 1 | 88 | 5.38 |
| Guillem Godoy | 2 | 220 | 21.72 |
| Albert Rubio | 3 | 228 | 19.44 |