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

De WikiGLC
Saltar a: navegación, buscar
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:
    • 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:
Obtenido de «https://www.glc.us.es/web/index.php?title=Proving_termination_with_multiset_orderings_in_PVS:_theory,_methodology_and_applications_(PROTEMO)&oldid=908»