Diferencia entre revisiones de «Theories»
(New page: == Theories == * [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 ...) |
(→Theories) |
||
| Línea 4: | Línea 4: | ||
* [http://www.cs.us.es/~jruiz/acl2-fot/ Reasoning about first-order terms using the ACL2 theorem prover] | * [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/~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/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] | ||
Revisión del 21:35 15 abr 2008
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).
