Diferencia entre revisiones de «Theories»
(→Theories) |
|||
| Línea 6: | Línea 6: | ||
* [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/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] | * [http://www.cs.us.es/~fmartin/acl2/dickson/ Formalization and proof of Dickson's Lemma in ACL2] | ||
| − | * [ | + | * [http://www.glc.us.es/theories/deltarule/CLAI2009.hs Implementation of Independence Rule] |
== Resources == | == Resources == | ||
Revisión del 00:40 9 nov 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
- 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.
