Diferencia entre revisiones de «Theories»
(→Resources) |
(→Theories in PVS) |
||
| (No se muestran 18 ediciones intermedias de 3 usuarios) | |||
| Línea 1: | Línea 1: | ||
== Theories == | == Theories == | ||
| − | + | === Theories in PVS === | |
| − | + | # [[A Formalization of Abstract Properties of Confluent Reductions in PVS]]. | |
| − | + | # [[Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)]]. | |
| − | + | # [[A formally verified prover for the ALC description logic in PVS]]. | |
| − | + | # [[Verification of the formal concept analysis in PVS]]. | |
| − | + | # [[A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution]]. | |
| − | + | # [[Theory of Refinements in PVS]]. | |
| − | + | ||
| + | === Theories in ACL2 === | ||
| + | # [http://www.cs.us.es/~jalonso/trabajos_dirigidos/Teoria_computacional_en_ACL2_sobre_calculos_proposicionales.zip Teoría computacional (en ACL2) sobre cálculos proposicionales]. | ||
| + | # [http://www.cs.us.es/~jruiz/acl2-rewr/ Formalizing equational reasoning and rewriting (using ACL2)] | ||
| + | # [http://www.cs.us.es/~jruiz/acl2-mul/ Multiset relations: a tool for proving termination (in ACL2)] | ||
| + | # [http://www.cs.us.es/~jruiz/acl2-fot/ Reasoning about first-order terms using the ACL2 theorem prover] | ||
| + | # [http://www.cs.us.es/~jruiz/unificacion-dag/ An unification algorithm in ACL2 using dags] | ||
| + | # [http://www.cs.us.es/~fmartin/acl2/gen-sat/ A generic framework for propositional SAT-provers (formalization in ACL2)] | ||
| + | # [http://www.cs.us.es/~fmartin/acl2/dickson/ Formalization and proof of Dickson's Lemma in ACL2] | ||
| + | === Theories in Haskell/QuickCheck === | ||
| + | # [http://www.glc.us.es/theories/deltarule/CLAI2009.hs Haskell implementation of Independence Rule] | ||
== Resources == | == Resources == | ||
| − | + | # [http://www.glc.us.es/apli2/ APLI2] (APLIcación de Ayuda Para Lógica Informática). | |
| − | + | # [[Stem]] Traducción de Base Stem(ConExp) a CLIPS. | |
| − | + | # [[Producciones]] Traducción de Reglas de Producción(ConExp) a CLIPS. | |
| − | + | # [[Delicioso]] Toma de datos y conversión en contexto (formato ConExp). | |
| − | + | # [[Paella]] Sistema visual de reparación de ontologías. | |
| − | + | # [[MenuXML]] Construcción de menus para móviles basado en FCA. | |
| + | # [[TinyDelicious]] Transformación de las URLs de Delicious en TinyUrls | ||
Revisión actual del 20:26 8 feb 2012
Sumario
Theories
Theories in PVS
- A Formalization of Abstract Properties of Confluent Reductions in PVS.
- Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO).
- A formally verified prover for the ALC description logic in PVS.
- Verification of the formal concept analysis in PVS.
- A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution.
- Theory of Refinements in PVS.
Theories in ACL2
- Teoría computacional (en ACL2) sobre cálculos proposicionales.
- Formalizing equational reasoning and rewriting (using ACL2)
- Multiset relations: a tool for proving termination (in ACL2)
- Reasoning about first-order terms using the ACL2 theorem prover
- An unification algorithm in ACL2 using dags
- A generic framework for propositional SAT-provers (formalization in ACL2)
- Formalization and proof of Dickson's Lemma in ACL2
Theories in Haskell/QuickCheck
Resources
- APLI2 (APLIcación de Ayuda Para Lógica Informática).
- Stem Traducción de Base Stem(ConExp) a CLIPS.
- Producciones Traducción de Reglas de Producción(ConExp) a CLIPS.
- Delicioso Toma de datos y conversión en contexto (formato ConExp).
- Paella Sistema visual de reparación de ontologías.
- MenuXML Construcción de menus para móviles basado en FCA.
- TinyDelicious Transformación de las URLs de Delicious en TinyUrls
