Diferencia entre revisiones de «Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)»

Revisión del 10:41 2 jun 2010

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:

@@ Línea 1: / Línea 1: @@
 {| border="1"
-| '''Title:''' Proving termination with multiset orderings in PVS: theory, methodology and applications
+| '''Title:'''
+| Proving termination with multiset orderings in PVS: theory, methodology and applications
 |-
-| '''Authors:''' {{jalonso}}, {{mjoseh}} y {{fmartin}}.
+| '''Authors:'''
+| {{jalonso}}, {{mjoseh}} y {{fmartin}}.
 |-
-| '''Date:''' November 2009.
+| '''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:
+| '''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 ...
+| '''Code:'''
+| You can find the PVS theories in ...
 |-
 | '''Documentation:'''
+|
+|}