Theories

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).