Diferencia entre revisiones de «A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution»
| Línea 1: | Línea 1: | ||
{| border="1" | {| border="1" | ||
| '''Title:''' | | '''Title:''' | ||
| − | | | + | | A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution. |
|- | |- | ||
| '''Authors:''' | | '''Authors:''' | ||
| − | | {{jalonso}}, {{mjoseh}} | + | | {{jalonso}}, {{mjoseh}}, {{fmartin}} y {{jruiz}}. |
|- | |- | ||
| '''Date:''' | | '''Date:''' | ||
| − | | | + | | 2001-2003. |
|- | |- | ||
| '''Description:''' | | '''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:''' | | '''Code:''' | ||
| Línea 16: | Línea 16: | ||
|- | |- | ||
| '''Documentation:''' | | '''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/Proving_termination_with_multiset_orderings_in_PVS.pdf Proving termination with multiset orderings in PVS: theory, methodology and applications] | ||
|} | |} | ||
Revisión del 11:21 2 jun 2010
| 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 in ... | |
| Documentation: | Papers and documents related with this work: | Proving termination with multiset orderings in PVS: theory, methodology and applications |
