Diferencia entre revisiones de «Theories»
(→Resources) |
(→Resources) |
||
Línea 10: | Línea 10: | ||
* [http://www.glc.us.es/apli2/ APLI2] (APLIcación de Ayuda Para Lógica Informática). | * [http://www.glc.us.es/apli2/ APLI2] (APLIcación de Ayuda Para Lógica Informática). | ||
* [http://www.glc.us.es/desarrollo/f2/ F2] (Implementación en Haskell de F2). | * [http://www.glc.us.es/desarrollo/f2/ F2] (Implementación en Haskell de F2). | ||
− | * [http://www.glc.us.es/desarrollo/ | + | * [http://www.glc.us.es/desarrollo/stem/ Stem] Traducción de Base Stem(ConExp) a CLIPS. |
* [http://www.glc.us.es/desarrollo/produccion/ Producción] Traducción de Reglas de Producción(ConExp) a CLIPS. | * [http://www.glc.us.es/desarrollo/produccion/ Producción] Traducción de Reglas de Producción(ConExp) a CLIPS. |
Revisión del 17:35 18 feb 2009
Theories
- 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
Resources
- APLI2 (APLIcación de Ayuda Para Lógica Informática).
- F2 (Implementación en Haskell de F2).
- Stem Traducción de Base Stem(ConExp) a CLIPS.
- Producción Traducción de Reglas de Producción(ConExp) a CLIPS.