Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq
In this thesis, we propose new automation capabilities for the Coq proof assistant. We obtain this mechanization via an integration into Coq of decision procedures for propositional logic, equality reasoning and linear arithmetic which make up the core of the Alt-Ergo SMT solver. This integration is...
| Main Author: | |
|---|---|
| Language: | English |
| Published: |
Université Paris Sud - Paris XI
2011
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00713668 http://tel.archives-ouvertes.fr/docs/00/71/36/68/PDF/VA2_LESCUYER_STEPHANE_04012011.pdf |