Theories

Theories

1. A Formalization of Abstract Properties of Confluent Reductions in PVS.
2. Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO).
3. A formally verified prover for the ALC description logic (in PVS).
4. Verification of the formal concept analysis in PVS.
5. A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution.
6. Theory of Refinements in PVS.
7. Teoría computacional (en ACL2) sobre cálculos proposicionales.
8. Formalizing equational reasoning and rewriting (using ACL2)
9. Multiset relations: a tool for proving termination (in ACL2)
10. Reasoning about first-order terms using the ACL2 theorem prover
11. An unification algorithm in ACL2 using dags
12. A generic framework for propositional SAT-provers (formalization in ACL2)
13. Formalization and proof of Dickson's Lemma in ACL2
14. Haskell implementation of Independence Rule

Resources

1. APLI2 (APLIcación de Ayuda Para Lógica Informática).
2. Stem Traducción de Base Stem(ConExp) a CLIPS.
3. Producciones Traducción de Reglas de Producción(ConExp) a CLIPS.
4. Delicioso Toma de datos y conversión en contexto (formato ConExp).
5. Paella Sistema visual de reparación de ontologías.
6. MenuXML Construcción de menus para móviles basado en FCA.
7. TinyDelicious Transformación de las URLs de Delicious en TinyUrls