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...)
 
 
(No se muestran 21 ediciones intermedias de 2 usuarios)
Línea 1: Línea 1:
−
* '''Title:''' A Formalization of Abstract Properties of Confluent Reductions in PVS
+
{| border="1"
−
* '''Autores:''' {{jalonso}} y {{mjoseh}}.
+
| '''Title:'''  
−
* '''Fecha de realización:''' Diciembre de 2009.
+
| Proving termination with multiset orderings in PVS: theory, methodology and applications
−
* '''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.
+
|-
−
* '''Code:''' La formalización en PVS se encuentra en ...
+
| '''Authors:'''  
−
* '''Documentation:'''
+
| {{jalonso}}, {{mjoseh}} and {{fmartin}}.
 +
|-
 +
| '''Date:'''  
 +
| November 2009.
 +
|-
 +
| '''Description:'''  
 +
| This theory presents 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 theorem of Dershowitz and Manna.
 +
# 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:
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-3.2/PROTEMO.tgz Version in PVS-3.2]
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-4.2/PROTEMO.tgz Version in PVS-4.2].
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-5.0/PROTEMO.tgz Version in PVS-5.0].
 +
|-
 +
| '''Documentation:'''
 +
| Papers and documents related with this work:
 +
*[http://www.cs.us.es/~mjoseh/pub/Proving_termination_with_multiset_orderings_in_PVS.pdf Proving termination with multiset orderings in PVS: theory, methodology and applications]
 +
*[http://www.cs.us.es/~mjoseh/pub/Well_founded_multiset_order.pdf Formalización en PVS de la buena fundamentación del orden de multiconjuntos]
 +
|}

Revisión actual del 14:19 8 feb 2012

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 presents a methodology to organize and simplify non-trivial termination proofs of functions using well-founded multiset orderings. The theory consists of:
  1. A formalization of the theorem of Dershowitz and Manna.
  2. A methodology for proving termination properties.
  3. 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:
Documentation: Papers and documents related with this work:
Obtenido de «https://www.glc.us.es/web/index.php?title=Proving_termination_with_multiset_orderings_in_PVS:_theory,_methodology_and_applications_(PROTEMO)&oldid=1123»