Automated Reasoning
Overview
Historically, automated reasoning is divided into two main
streams, the first one is based on resolution, rewriting and
unification techniques, and the second one on the combination of
decision procedures. For twenty years, our team has been working on
rewriting and has developed the rewriting tool box
CiME, as well
as its Coq certification library
Coccinelle. More recently, we
have been interested in the second approach, and we started the
development of the SMT prover
AltErgo. One of our current goals
is to integrate rewriting techniques at the very heart of
AltErgo, in order to increase both its efficiency and
expressivity.
Thematics
Rewriting
Term rewriting is a way to tackle equality in the automated deduction
field: whereas an equation can be used in either directions, a
rewriting rule can be used only from left to right.
For instance, the following system models the nonabelian groups using
the usual mathematical definition:
(x . y) . z  =  x . (y . z)  (A) 
x . e  =  x  (N) 
x . i(x)  =  e  (I) 

Whith these equalities, it is possible to prove that
i(
e) =
e by the following steps:
i(e)  =_{N}  i(e) . e 
 =_{I}  i(e) . (i(e) . i(i(e))) 
 =_{N}  i(e) . (i(e) . i(i(e).e)) 
 =_{I}  i(e) . (i(e) . i(i(e).(e.i(e)))) 
 =_{A}  i(e) . (i(e) . i((i(e).e).i(e))) 
 =_{N}  i(e). (i(e) . i( i(e).i(e) )) 
 =_{A}  (i(e). i(e)) . i( i(e).i(e) )) 
 =_{I}  e 

Restricting the above set of equalities to the rewriting system displayed below
raises several issues.
(x . y) . z  →  x . (y . z)  (A) 
x . e  →  x  (N) 
x . i(x)  →  e  (I) 

First, it is no longer possible to prove that
i(
e) =
e, since none of the two terms can be reduced. The second
problem is how to garantee that reducing as far as possible a term
will eventually yield a result in a finite time. The corresponding
properties are kown as confluence and termination.
Completion is a way of recovering confluence, but the process may not
terminate, and yields only a semidecision procedure.
Since the last decade, termination is a very active area in automated
deduction: numerous criteria have been proposed, and implemented in
several tools. Since 2003, there is a termination competition which reveals
that every participant tool has at least once used a non valid argument in
its proofs.
We work on how to certify some of the algorithms used in rewriting
tools, and also some properties of rewriting systems, such as equality
modulo and termination. For that purpose, we developp
Coccinelle, the Coq
companion library of our rewriting tool box
CiME.
Coccinelle features
the Coq modelling of :
 terms and rewriting;
 some key algorithms of CiME, such as
 unification;
 matching modulo associative and commutative symbols;
 RPO ordering;
 powerfull termination criteria;
Hence
Coccinelle can be used to check that a termination certificate is valid,
that is when a theorem is applied, all its premises are fullfilled.
Combination of Decision Procedures
AltErgo is an SMT (Satisfiability Modulo Theory) solver
dedicated to program verification. The input syntax of
AltErgo is a
first order logic extended with predefined theories and polymorphic
types. The builtin theories of
AltErgo are the following:
 equality with uninterpreted symbols;
 arithmetic over the rationals and the integers;
 a polymorphic arrays;
 fixed size bitvectors;
 enumeration types;
 associative and commutative symbols.
People
François Bobot,
Sylvain Conchon,
Évelyne Contejean,
Claire Dross,
Mohamed Iguernelala,
Alain Mebsout,
Andrei Paskevich,
Xavier Urbain
Tools
 AltErgo,
an SMT solver dedicated to program verification
 CiME,
a rewriting tool box
 Coccinelle,
its Coq library companion
Grants
Main publications
 [1]
 Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala.
Canonized Rewriting and Ground AC Completion Modulo Shostak
Theories. In Parosh A. Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Saarbrücken, Germany, April 2011. Springer.
[ bib ]
 [2]
 Stéphane Lescuyer and Sylvain Conchon.
Improving Coq propositional reasoning using a lazy CNF conversion
scheme. In Silvio Ghilardi and Roberto Sebastiani, editors, Frontiers of
Combining Systems, 7th International Symposium, Proceedings, volume 5749 of Lecture Notes in Computer Science, pages 287303, Trento, Italy,
September 2009. Springer.
[ bib 
DOI ]
 [3]
 François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane
Lescuyer.
Implementing Polymorphism in SMT solvers.
In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th
International Workshop on Satisfiability Modulo, volume 367 of ACM
International Conference Proceedings Series, pages 15, 2008.
[ bib 
PDF 
.pdf ]
 [4]
 Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
CC(X): Semantical combination of congruence closure with solvable
theories.
In Proceedings of the 5th International Workshop on
Satisfiability Modulo Theories (SMT 2007), volume 1982 of Electronic
Notes in Computer Science, pages 5169. Elsevier Science Publishers, 2008.
[ bib ]
 [5]

Stéphane Lescuyer and Sylvain Conchon.
A reflexive formalization of a SAT solver in Coq.
In Emerging Trends of the 21st International Conference on
Theorem Proving in Higher Order Logics, 2008.
[ bib ]