Diferencia entre revisiones de «A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution»

De WikiGLC
Saltar a: navegación, buscar
(New page: * '''Title:''' * '''Autores:''' {{jalonso}} y {{mjoseh}}. * '''Fecha de realización:''' * '''Abstract:''' * '''Code:''' You can find the PVS theories in ... * '''Documentation:''')
 
 
(No se muestran 9 ediciones intermedias de 2 usuarios)
Línea 1: Línea 1:
−
* '''Title:'''  
+
{| border="1"
−
* '''Autores:''' {{jalonso}} y {{mjoseh}}.
+
| '''Title:'''  
−
* '''Fecha de realización:'''  
+
| A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution.
−
* '''Abstract:'''  
+
|-
−
* '''Code:''' You can find the PVS theories in ...
+
| '''Authors:'''  
−
* '''Documentation:'''
+
| {{jalonso}}, {{mjoseh}}, {{fmartin}} y {{jruiz}}.
 +
|-
 +
| '''Date:'''  
 +
| 2001-2003.
 +
|-
 +
| '''Description:'''  
 +
| This theory presents a proof in PVS of the Strong Completeness of SLD-Resolution for the propositional logic. We have formalized the propositional logic programming and we have proof the equivalence between the differents semantics of the logic programs. We also transform the previous specifications of Propositional Logic into their respective executable specifications by using [[Theory of Refinements in PVS|refinements]]. Finally, we verify several refutation algorithms based on breadth search, depth search and depth iterative search.
 +
|-
 +
| '''Code:'''  
 +
| You can find the PVS theories
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-3.2/pl.tgz Version PVS-3.2].
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-4.2/pl.tgz Version PVS-4.2].
 +
* [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-5.0/pl.tgz Version PVS-5.0].
 +
|-
 +
| '''Documentation:'''
 +
| Papers and documents related with this work:
 +
* [http://www.cs.us.es/~jalonso/trabajos_dirigidos/2004-tesis-MJHD.pdf Teoría computacional (en PVS) de la programación lógica y del análisis formal de conceptos] (Tesis, Universidad de Sevilla, 2004).
 +
* [http://www.cs.us.es/~mjoseh/pub/A_formally_verified_proof_PVS_strong_completeness_propositional_SLD_resolution.pdf A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution].
 +
|}

Revisión actual del 13:16 4 oct 2011

Title: A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution.
Authors: José A. Alonso, María J. Hidalgo, Francisco J. Martín y José L. Ruiz Reina.
Date: 2001-2003.
Description: This theory presents a proof in PVS of the Strong Completeness of SLD-Resolution for the propositional logic. We have formalized the propositional logic programming and we have proof the equivalence between the differents semantics of the logic programs. We also transform the previous specifications of Propositional Logic into their respective executable specifications by using refinements. Finally, we verify several refutation algorithms based on breadth search, depth search and depth iterative search.
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=A_formally_verified_proof_in_PVS_of_the_strong_completeness_theorem_of_propositional_SLD-resolution&oldid=1035»