Return to search

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 achieved through the reflection technique, which consists in implementing and formally proving these algorithms in Coq in order to execute them directly in the proof assistant. Because the algorithms formalized in Coq are exactly those in use in Alt-Ergo's kernel, this work significantly increases our trust in the solver. In particular, it embeds an original algorithm for combining equality modulo theory reasoning, called CC(X) and inspired by the Shostak combination algorithm, and whose justification is quite complex. Our Coq implementation is available in the form of tactics which allow one to automatically solve formulae combining propositional logic, equality and arithmetic. In order to make these tactics as efficient as may be, we have taken special care with performance in our implementation, in particular through the use of classical efficient data structures, which we provide as a separate library.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00713668
Date04 January 2011
CreatorsLescuyer, Stephane
PublisherUniversité Paris Sud - Paris XI
Source SetsCCSD theses-EN-ligne, France
LanguageEnglish
Detected LanguageEnglish
TypePhD thesis

Page generated in 0.0019 seconds