Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)

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: Version in PVS-3.2 Version in PVS-4.2.
Documentation:	Papers and documents related with this work: Proving termination with multiset orderings in PVS: theory, methodology and applications Formalización en PVS de la buena fundamentación del orden de multiconjuntos