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 Alt-Ergo
. One of our current goals
is to integrate rewriting techniques at the very heart of
, in order to increase both its efficiency and
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 non-abelian 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
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) )) |
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
, 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 semi-decision 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
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
the Coq modelling of :
- terms and rewriting;
- some key algorithms of CiME, such as
- matching modulo associative and commutative symbols;
- RPO ordering;
- powerfull termination criteria;
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
is an SMT (Satisfiability Modulo Theory) solver
dedicated to program verification. The input syntax of Alt-Ergo
first order logic extended with predefined theories and polymorphic
types. The built-in theories of Alt-Ergo
are the following:
- equality with uninterpreted symbols;
- arithmetic over the rationals and the integers;
- a polymorphic arrays;
- fixed size bit-vectors;
- enumeration types;
- associative and commutative symbols.
an SMT solver dedicated to program verification
a rewriting tool box
its Coq library companion
- 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 ]
- 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 287-303, Trento, Italy,
September 2009. Springer.
[ bib |
- François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane
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 1-5, 2008.
[ bib |
- Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
CC(X): Semantical combination of congruence closure with solvable
In Proceedings of the 5th International Workshop on
Satisfiability Modulo Theories (SMT 2007), volume 198-2 of Electronic
Notes in Computer Science, pages 51-69. Elsevier Science Publishers, 2008.
[ bib ]
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 ]