Diferencia entre revisiones de «Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)»
Línea 10: | Línea 10: | ||
|- | |- | ||
| '''Description:''' | | '''Description:''' | ||
− | | This theory | + | | 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 Dershowitz and Manna | + | # A formalization of the theorem of Dershowitz and Manna. |
# A methodology for proving termination properties. | # 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 | # 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 |
Revisión del 15:27 2 jun 2010
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:
|
Code: | You can find the PVS theories here. |
Documentation: | Proving termination with multiset orderings in PVS: theory, methodology and applications |