| Title:
|
Proving termination with multiset orderings in PVS: theory, methodology and applications
|
| Authors:
|
José A. Alonso, María J. Hidalgo and Francisco J. Martín.
|
| Date:
|
November 2009.
|
| Description:
|
This theory presents a methodology to organize and simplify non-trivial termination proofs of functions using well-founded multiset orderings. The theory consists of:
- A formalization of the theorem of Dershowitz and Manna.
- A methodology for proving termination properties.
- Three case studies: a tail-recursive definition of Ackermann's function, an iterative definition of McCarthy's 91 function and an iterative function to compute a generic schema for double recursion
|
| Code:
|
You can find the PVS theories:
|
| Documentation:
|
Papers and documents related with this work:
|
