Ph.D

Group : Toccata

*Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq*
Starts on 16/07/2007

Advisor : CONTEJEAN, Evelyne

**Funding :** CDD sur contrat INRIA

**Affiliation :** Université Paris-Sud

**Laboratory :** LRI-INRIA PROVAL

**Defended** on 04/01/2011, committee :

Rapporteurs

Pierre Crégut (Orange Labs)

Shankar Natarajan (SRI)

Examinateurs

Hugo Herbelin (INRIA)

Sava Krstic (Intel)

Burkhart Wolff (Paris-Sud)

Encadrants

Evelyne Contejean (CNRS)

Sylvain Conchon (Paris-Sud)

**Research activities :**
**Abstract :**
n 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.