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

• 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: