Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq
Dans cette thèse, nous proposons une amélioration de l'automatisation des preuves dans l'assistant de preuve Coq. Cette automatisation est obtenue en intégrant à Coq les procédures de décision pour la logique propositionnelle, l'égalité et l'arithmétique linéaire constituant le n...
| Main Author: | |
|---|---|
| Other Authors: | |
| Language: | en |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://www.theses.fr/2011PA112363/document |