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
Alt-Ergo. One of our current goals
is to integrate rewriting techniques at the very heart of
Alt-Ergo, 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 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(
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 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
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
Alt-Ergo is an SMT (Satisfiability Modulo Theory) solver
dedicated to program verification. The input syntax of
Alt-Ergo is a
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.
People
François Bobot,
Sylvain Conchon,
Évelyne Contejean,
Claire Dross,
Mohamed Iguernelala,
Alain Mebsout,
Andrei Paskevich,
Xavier Urbain
Tools
- Alt-Ergo,
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 287-303, 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 1-5, 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 198-2 of Electronic
Notes in Computer Science, pages 51-69. 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 ]