Diferencia entre revisiones de «Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)»
| Línea 11: | Línea 11: | ||
| '''Description:''' | | '''Description:''' | ||
| This theory present a methodology to organize and simplify non-trivial termination proofs of functions using well-founded multiset orderings. The theory consists of: | | 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:''' | | '''Code:''' | ||
Revisión del 10:41 2 jun 2010
| Title: | Proving termination with multiset orderings in PVS: theory, methodology and applications |
| Authors: | José A. Alonso, María J. Hidalgo y Francisco J. Martín. |
| Date: | November 2009. |
| Description: | This theory present a methodology to organize and simplify non-trivial termination proofs of functions using well-founded multiset orderings. The theory consists of:
|
| Code: | You can find the PVS theories in ... |
| Documentation: |
