Theories

Theories

Theories in PVS

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.

Theories in ACL2

1. Teoría computacional (en ACL2) sobre cálculos proposicionales.
2. Formalizing equational reasoning and rewriting (using ACL2)
3. Multiset relations: a tool for proving termination (in ACL2)
4. Reasoning about first-order terms using the ACL2 theorem prover
5. An unification algorithm in ACL2 using dags
6. A generic framework for propositional SAT-provers (formalization in ACL2)
7. Formalization and proof of Dickson's Lemma in ACL2

Theories in Haskell/QuickCheck

1. 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