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 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 here.
Documentation:	Proving termination with multiset orderings in PVS: theory, methodology and applications