Diferencia entre revisiones de «Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)»
| Línea 4: | Línea 4: | ||
* '''Abstract:''' This theory present a methodology to organize and simplify non-trivial termination proofs of functions using well-founded multiset orderings. The theory consists of: | * '''Abstract:''' This theory present 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 Dershowitz and Manna theorem. | ** A formalization of the Dershowitz and Manna theorem. | ||
| − | + | ** 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 in ... | * '''Code:''' You can find the PVS theories in ... | ||
* '''Documentation:''' | * '''Documentation:''' | ||
Revisión del 19:11 1 jun 2010
- Title: Proving termination with multiset orderings in PVS: theory, methodology and applications
- Autores: José A. Alonso y María J. Hidalgo.
- Fecha de realización: Noviembre de 2009.
- Abstract: This theory present 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 Dershowitz and Manna theorem.
- 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 in ...
- Documentation:
