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

De WikiGLC
Saltar a: navegación, buscar
(New page: * '''Title:''' A Formalization of Abstract Properties of Confluent Reductions in PVS * '''Autores:''' {{jalonso}} y {{mjoseh}}. * '''Fecha de realización:''' Diciembre de 2009. * '''Abstr...)
 
Línea 1: Línea 1:
−
* '''Title:''' A Formalization of Abstract Properties of Confluent Reductions in PVS
+
* '''Title:''' Proving termination with multiset orderings in PVS: theory, methodology and applications
 
* '''Autores:''' {{jalonso}} y {{mjoseh}}.
 
* '''Autores:''' {{jalonso}} y {{mjoseh}}.
−
* '''Fecha de realización:''' Diciembre de 2009.
+
* '''Fecha de realización:''' Noviembre de 2009.
−
* '''Abstract:''' This theory is a simple and smart formalization of abstract confluence properties such Newman's Lemma or the Church-Rosser property. This formalization is based on the paper "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems " of G. Huet.
+
* '''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:
−
* '''Code:''' La formalización en PVS se encuentra en ...
+
 
 +
            + 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:'''
 
* '''Documentation:'''

Revisión del 19:09 1 jun 2010

  • 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:
Obtenido de «https://www.glc.us.es/web/index.php?title=Proving_termination_with_multiset_orderings_in_PVS:_theory,_methodology_and_applications_(PROTEMO)&oldid=880»