Diferencia entre revisiones de «Theories»
| Línea 2: | Línea 2: | ||
* [[A Formalization of Abstract Properties of Confluent Reductions in PVS]]. | * [[A Formalization of Abstract Properties of Confluent Reductions in PVS]]. | ||
* [[Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)]]. | * [[Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)]]. | ||
| + | * [[A formally verified prover for the ALC description logic (or Constructing formally verified reasoners for the ALC description logic)]]. | ||
| + | * [[Verification of the formal concept analysis in PVS]]. | ||
| + | * [[A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution]]. | ||
| + | * [[Refinements]]. | ||
* [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/~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-rewr/ Formalizing equational reasoning and rewriting (using ACL2)] | ||
Revisión del 19:32 1 jun 2010
Theories
- 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 (or Constructing formally verified reasoners for the ALC description logic).
- Verification of the formal concept analysis in PVS.
- A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution.
- Refinements.
- 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
- Haskell implementation of Independence Rule
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
