@ARTICLE{conchon08entcs,
AUTHOR = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig and St\'ephane Lescuyer},
TITLE = {{CC(X): Semantical Combination of Congruence Closure with
Solvable Theories}},
BOOKTITLE = {Proceedings of the 5th International Workshop on
Satisfiability Modulo Theories ({SMT 2007})},
JOURNAL = {Electronic Notes in Computer Science},
PUBLISHER = {Elsevier},
VOLUME = {198},
NUMBER = {2},
PAGES = {51--69},
YEAR = 2008,
ABSTRACT = {
We present a generic congruence closure algorithm for deciding
ground formulas in the combination of the theory of equality with
uninterpreted symbols and an arbitrary built-in solvable theory X.
Our algorithm CC(X) is reminiscent of Shostak combination: it
maintains a union-find data-structure modulo X from which maximal
information about implied equalities can be directly used for
congruence closure. CC(X) diverges from Shostak's approach by the use
of semantical values for class representatives instead of canonized
terms. Using semantical values truly reflects the actual
implementation of the decision procedure for X. It also enforces to
entirely rebuild the algorithm since global canonization, which is
at the heart of Shostak combination, is no longer feasible with
semantical values. CC(X) has been implemented in Ocaml and is at
the core of Ergo, a new automated theorem prover dedicated to
program verification.
},
TOPICS = {team},
TYPE_PUBLI = {irevcomlec},
X-EQUIPES = {demons PROVAL},
X-TYPE = {article},
X-SUPPORT = {actes},
X-CLE-SUPPORT = {ENTCS},
X-EDITORIAL-BOARD = {yes},
X-INTERNATIONAL-AUDIENCE = {yes},
X-PROCEEDINGS = {yes}
}
@INPROCEEDINGS{conchon08smt,
AUTHOR = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean
and St\'ephane Lescuyer},
TITLE = {{Implementing Polymorphism in SMT solvers}},
BOOKTITLE = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
YEAR = 2008,
EDITOR = {Clark Barrett and Leonardo de Moura},
TOPICS = {team,lri},
TYPE_DIGITEO = {conf_autre},
TYPE_PUBLI = {colloque},
X-EQUIPES = {demons PROVAL},
X-TYPE = {article},
X-SUPPORT = {actes_aux},
X-CLE-SUPPORT = {SMT},
X-PDF = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
X-EDITORIAL-BOARD = {yes},
X-INTERNATIONAL-AUDIENCE = {yes},
X-PROCEEDINGS = {yes}
}
@INPROCEEDINGS{conchon07afm,
AUTHOR = {Sylvain Conchon and Evelyne Contejean and Johannes Kannig and St{\'e}phane Lescuyer},
TITLE = {{Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant}},
BOOKTITLE = {{AFM07 (Automated Formal Methods)}},
YEAR = 2007,
EDITOR = {John Rushby and N. Shankar},
ABSTRACT = {Ergo is a little engine of proof dedicated to program
verification. It fully supports quantifiers and directly handles
polymorphic sorts. Its core component is CC(X), a new combination
scheme for the theory of uninterpreted symbols parameterized by a
built-in theory X. In order to make a sound integration in a proof
assistant possible, Ergo is capable of generating proof traces
for CC(X). Alternatively, Ergo can also be called interactively
as a simple oracle without further verification. It is currently
used to prove correctness of C and Java programs as part of the Why
platform.}
}
@INPROCEEDINGS{contejean07frocos,
AUTHOR = {Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
TITLE = {{Certification of automated termination proofs}},
BOOKTITLE = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
YEAR = 2007,
EDITOR = {Boris Konev and Frank Wolter},
VOLUME = 4720,
PAGES = {148--162},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Liverpool,UK},
MONTH = SEP,
PUBLISHER = {Springer},
ABSTRACT = {Nowadays, formal methods rely on tools of different kinds: proof
assistants with which the user interacts to discover a proof step by
step; and fully automated tools which make use of (intricate)
decision procedures. But while some proof assistants can
\emph{check} the soundness of a proof, they lack automation.
Regarding automated tools, one still has to be satisfied with their
answers \texttt{Yes}/\texttt{No}/\texttt{Do\,not\,know}, the validity
of which can be subject to question, in particular because of the
increasing size and complexity of these tools.
In the context of rewriting techniques, we aim at bridging the gap
between proof assistants that yield formal guarantees of reliability
and highly automated tools one has to trust. We present an approach
making use of both shallow and deep embeddings. We illustrate this
approach with a prototype based on the CiME rewriting toolbox,
which can discover involved termination proofs that can be
certified by the coq proof assistant, using the Coccinelle
library for rewriting.}
}
@INPROCEEDINGS{conchon07smt,
AUTHOR = {Sylvain Conchon and Evelyne Contejean and Johannes Kanig},
TITLE = {{CC(X): Efficiently Combining Equality and Solvable Theories without Canonizers}},
BOOKTITLE = {SMT 2007: 5th International Workshop on Satisfiability Modulo},
YEAR = 2007,
EDITOR = {Sava Krstic and Albert Oliveras},
ABSTRACT = { We present a generic congruence closure algorithm for deciding
ground formulas in the combination of the theory of equality with
uninterpreted symbols and a union $X$ of solvable theories. Our
algorithm $cc(X)$ is reminiscent of Shostak combination: it maintains
a union-find data-structure modulo $X$ from which maximal
information about implied equalities can be directly used for
congruence closure. $cc(X)$ diverges from Shostak approach by the
use of semantical values for class representatives instead of
syntactical canonizers. This seemingly insignificant difference has
strong impact on efficiency and expressiveness. It also enforces to
entirely rebuild the algorithm since global canonization, which is
at the heart of Shostak combination, is no longer feasible with
semantical values. $cc(X)$ has been implemented in Ocaml and is
at the core of Ergo, a new automated theorem prover dedicated to
program verification.
}
}
@INPROCEEDINGS{contejean07jpj,
AUTHOR = {{Evelyne Contejean}},
EDITOR = {{Hubert Comon-Lundth and Claude Kirchner and Hélène Kirchner}},
BOOKTITLE = {{Rewriting, Computation and Proof}},
TITLE = {{Modelling permutations in COQ for Coccinelle}},
PUBLISHER = {Springer},
YEAR = 2007,
VOLUME = 4600,
SERIES = {Lecture Notes in Computer Science},
NOTE = {Jouannaud Festschrift},
ABSTRACT = {In this paper we present the part of the Coccinelle library which
deals with list permutations. Indeed permutations naturally arise
when formally modeling rewriting in COQ, for instance RPO with
multiset status and equality modulo AC. Moreover the needed
permutations are up to an equivalence relation, and may be used to
inductively define the same relation (equivalence modulo RPO). This
is why we introduce the notion of permutation w. r. t. an arbitrary
relation. The advantages of our approach are a very simple inductive
definition (with only 2 constructors), the adequacy with the
mathematical definition, the ability to define a relation using
recursively permutations up to this very relation, and a fine
grained modularity (if $\mathtt{R}$ enjoys a property, so does
$\mathtt{permut~R}$).
}
}
@TECHREPORT{contejean07rr,
AUTHOR = {Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
TITLE = {{Certification of automated termination proofs}},
INSTITUTION = {CEDRIC},
YEAR = 2007,
NUMBER = 1185,
MONTH = MAY
}
@MISC{ergo,
AUTHOR = {Sylvain Conchon and Evelyne Contejean},
TITLE = {{The Ergo automatic Theorem Prover}},
YEAR = 2006,
URL = {http://ergo.lri.fr}
}
@MISC{coccinelle,
AUTHOR = {Evelyne Contejean},
TITLE = {{Coccinelle}},
YEAR = 2005,
URL = {http://www.lri.fr/~contejea/Coccinelle/coccinelle.html}
}
@ARTICLE{contejean05jar,
AUTHOR = {Evelyne Contejean and Claude March{\'e} and Ana Paula Tom{\'a}s and Xavier Urbain},
TITLE = {{Mechanically proving termination using polynomial
interpretations}},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {34},
NUMBER = {4},
PAGES = {325--363},
YEAR = 2005,
ABSTRACT = {For a long time, term orderings defined by polynomial
interpretations have been considered far too restrictive to be used
for computer-aided termination proof of TRSs. But recently, the
introduction of the dependency pairs approach achieved considerable
progress w.r.t. automated termination proof, in particular by
requiring from the underlying ordering much weaker properties
than the classical approach. As a consequence, the noticeable power
of a combination \mbox{dependency pairs/polynomial orderings}
yielded a regain of interest for these interpretations.
We describe criteria on polynomial interpretations for
them to define weakly monotonic orderings. From these criteria, we
obtain new techniques both for mechanically checking termination
using a given polynomial interpretation, and for
finding such interpretations with full automation. With regards to
automated search, we propose an original method for solving
Diophantine constraints.
We implemented these techniques into the CiME rewrite tool, and we
provide experimental results that show how useful polynomial orderings
actually are in practice.},
URL = {http://dx.doi.org/10.1007/s10817-005-9022-x}
}
@INPROCEEDINGS{contejean05cade,
AUTHOR = {Evelyne Contejean and Pierre Corbineau},
TITLE = {{Reflecting Proofs in First-Order Logic with Equality}},
PAGES = {7--22},
BOOKTITLE = {20th International Conference on Automated Deduction (CADE-20)},
ADDRESS = {Tallinn, Estonia},
MONTH = JUL,
YEAR = 2005,
EDITOR = {Robert Nieuwenhuis},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 3632,
PUBLISHER = {Springer},
ABSTRACT = {Our general goal is to provide better automation in interactive proof
assistants such as Coq.
We present an interpreter of proof traces in first-order multi-sorted
logic with equality. Thanks to the reflection ability of Coq, this
interpreter is both implemented and formally
proved sound --- with respect to a reflective interpretation of formulae
as Coq properties --- inside Coq's type theory.
Our generic framework allows to interpret proofs traces computed by
any automated theorem prover, as long as they are precise enough: we
illustrate that on traces produced by the CiME tool when solving
unifiability problems by ordered completion. We discuss
some benchmark results obtained on the TPTP library.}
}
@TECHREPORT{contejean04rr,
AUTHOR = {Evelyne Contejean and Claude March{\'e} and Ana-Paula Tom{\'a}s and Xavier Urbain},
TITLE = {{Mechanically proving termination using polynomial interpretations}},
INSTITUTION = {LRI},
YEAR = {2004},
TYPE = {Research Report},
NUMBER = {1382},
URL = {http://www.lri.fr/~urbain/textes/rr1382.ps.gz}
}
@INPROCEEDINGS{contejean04rta,
AUTHOR = {Evelyne Contejean},
TITLE = {{A certified AC matching algorithm}},
BOOKTITLE = {15th International Conference on Rewriting Techniques and Applications},
EDITOR = {Vincent van Oostrom},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 3091,
MONTH = JUN,
YEAR = 2004,
ADDRESS = {Aachen, Germany},
PAGES = {70--84},
ABSTRACT = { In this paper, we propose a matching algorithm for terms containing
some function symbols which can be either free, commutative or
associative-commutative. This algorithm is presented by inference
rules and these rules have been formally proven sound and complete,
and decreasing in the coq proof assistant while the corresponding
algorithm is implemented in the CiME system. Moreover some
preparatory work has been done in coq, such as proving that checking
the equality of two terms modulo some commutative and
associative-commutative theories is decidable.}
}
@MISC{cime3,
AUTHOR = {Evelyne Contejean and Claude March{\'e} and
Xavier Urbain},
TITLE = {{CiME3}},
NOTE = {Available at
\url{http://cime.lri.fr/}},
YEAR = 2004,
URL = {http://cime.lri.fr/}
}
@INPROCEEDINGS{contejean03wst,
AUTHOR = {Evelyne Contejean and Claude March{\'e} and Benjamin Monate and Xavier Urbain},
TITLE = {{Proving Termination of Rewriting with {\sc C\textit{i}ME}}},
PAGES = {71--73},
YEAR = 2003,
URL = {http://cime.lri.fr},
NOTE = {\url{http://cime.lri.fr}},
BOOKTITLE = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
EDITOR = {Albert Rubio},
MONTH = JUN,
NOTE = {Technical Report DSIC II/15/03, Universidad Polit\'ecnica de Valencia, Spain}
}
@INPROCEEDINGS{boudet01rta,
AUTHOR = {Alexandre Boudet and Evelyne Contejean},
TITLE = {{Combining Pattern $E$-unification Algorithms}},
BOOKTITLE = {12th International Conference on Rewriting Techniques and Applications},
EDITOR = {Aart Middeldorp},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 2051,
MONTH = MAY,
YEAR = 2001,
ADDRESS = {Utrecht, The Netherlands},
PAGES = {63--76},
ABSTRACT = {We present an algorithm for unification of higher-order patterns
modulo combinations of disjoint first-order equational theories. This
algorithm is highly non-deterministic, in the spirit of those by
Schmidt-Schau\ss and Baader-Schulz in the first-order case.
%
We redefine the properties required for elementary pattern unification
algorithms of pure problems in this context, then we show that some
theories of interest have elementary unification algorithms fitting
our requirements.
%
This provides a unification algorithm for patterns modulo the
combination of theories such as the free theory, commutativity,
one-sided distributivity, associativity-commutativity and some of its
extensions, including Abelian groups.}
}
@INPROCEEDINGS{contejean01symcon,
AUTHOR = {Evelyne Contejean and Ana Paula Tomas},
TITLE = {{On Symmetries in Systems Coming from AC-Unification of
Higher-Order Patterns}},
BOOKTITLE = {{SymCon'01, Symmetry in Constraints}},
YEAR = 2001,
EDITOR = {Pierre Flener and Justin Pearson},
ADDRESS = {Paphos, Cyprus},
MONTH = DEC
}
@INPROCEEDINGS{contejean00rta,
AUTHOR = {Evelyne Contejean and Antoine Coste and Benjamin Monate},
TITLE = {Rewriting Techniques in Theoretical Physics},
PAGES = {80--94},
BOOKTITLE = {11th International Conference on Rewriting Techniques and Applications},
EDITOR = {Leo Bachmair},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1833,
MONTH = JUL,
YEAR = 2000,
ADDRESS = {Norwich, UK},
ABSTRACT = {This paper presents a general method for studying some quotients of
the special linear group $SL_2$ over the integers, which are of
fundamental interest in the field of statistical physics. Our method
automatically helps in validating some conjectures due to physicists,
such as conjectures stating that a set of equations completely
describes a finite given quotient of $SL_2({\mathbb Z})$. In a first step, we show
that in the cases we are interested in, the usual presentation of
finitely generated groups with some constant generators and a binary
concatenation can be turned into an equivalent one with unary
generators. In a second step, when the completion of the transformed
set of equations terminates, we show how to compute {\em directly} the
associated normal forms automaton. According to the presence of
loops, we are able to decide the finiteness of the quotient, and to
compute its cardinality. When the quotient is infinite, the automaton
gives some hints on what kind of equations are needed in order to
insure the finiteness of the quotient.}
}
@MISC{cime2,
AUTHOR = {Evelyne Contejean and Claude March{\'e} and
Benjamin Monate and Xavier Urbain},
TITLE = {{CiME version 2}},
NOTE = {Available at
\url{http://cime.lri.fr/}},
YEAR = 2000,
URL = {http://cime.lri.fr/}
}
@INPROCEEDINGS{beldiceanu98informs,
AUTHOR = {Nicolas Beldiceanu and Eric Bourreau and Evelyne Contejean},
TITLE = {Solving a Hard Vehicle Routing and Loading Problem},
BOOKTITLE = {Proceedings of the Spring Meeting of the Institute for
Operations Research and the Management Sciences},
YEAR = 1998,
ADDRESS = {Montreal},
MONTH = APR
}
@INPROCEEDINGS{boudet98cade,
AUTHOR = {Alexandre Boudet and Evelyne Contejean},
TITLE = {{About the Confluence of Equational Pattern Rewrite
Systems}},
EDITOR = {C. and H. Kirchner},
BOOKTITLE = {15th International Conference on Automated Deduction},
YEAR = 1998,
PAGES = {88--102},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 1421,
ABSTRACT = {We study the confluence of higher-order pattern
rewrite systems modulo an equational theory $E$. This problem has been
investigated by Mayr and Nipkow, for the case of
rewriting modulo a congruence {\em \`a la} Huet, (in
particular, the equations of $E$ can be applied {\em above} the position
where a rewrite rule is applied). The case we address here is
rewriting using matching modulo $E$ as done in the first-order case
by Jouannaud and Kirchner.
The theory is then applied to the case of $AC$-theories, for which we
provided a complete unification algorithm in. It
happens that the $AC$-unifiers may have to be constrained by some
flexible-flexible equations of the form $\lambda x_1\cdots\lambda x_n.F(x_1,\ldots,
x_n)=\lambda x_1\cdots\lambda x_nF(x_{\sigma(1)},\ldots,x_{\sigma(n)})$, where $F$ is a free variable
and $\sigma$ a permutation. This situation requires a slight technical
adaptation of the theory.}
}
@ARTICLE{ajili97tcs,
AUTHOR = {Ajili, Farid and Contejean, Evelyne},
TITLE = {Avoiding Slack Variables in the Solving of Linear
Diophantine Equations and Inequations},
JOURNAL = TCS,
YEAR = 1997,
VOLUME = 173,
NUMBER = 1,
MONTH = FEB,
PAGES = {183--208},
EDITOR = {U. Montanari and F. Rossi},
FTP = {ftp://ftp.lri.fr/LRI/articles/contejean/tcs97.ps.gz},
ABSTRACT = {In this paper, we present an algorithm for solving {\em directly}
linear Diophantine systems of both equations and inequations. Here
directly means without adding slack variables for encoding
inequalities as equalities. This algorithm is an extension of the
algorithm due to Contejean and Devie \cite{contejean94ic} for solving
linear Diophantine systems of equations, which is itself a
generalization of the algorithm of Fortenbacher for
solving a single linear Diophantine equation. All the nice properties
of the algorithm of Contejean and Devie are still satisfied by the new
algorithm: it is complete, {\em i.e.} provides a (finite) description
of the set of solutions, it can be implemented with a {\em bounded}
stack, and it admits an incremental version. All of these
characteristics enable its easy integration in the CLP paradigm.},
ANNOTE = {Special Issue of TCS dedicated to a refereed
selection of papers presented at CP'95}
}
@INPROCEEDINGS{boudet97cp,
AUTHOR = {Alexandre Boudet and Evelyne Contejean},
TITLE = {{AC}-Unification of Higher-order Patterns},
BOOKTITLE = {Principles and Practice of Constraint Programming},
EDITOR = {Gert Smolka},
PUBLISHER = {Springer},
ADDRESS = {Linz, Austria},
MONTH = OCT,
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1330,
YEAR = 1997,
FTP = {ftp://ftp.lri.fr/LRI/articles/contejea/cp97.ps.gz},
ABSTRACT = {We present a complete algorithm for the unification of higher-order
patterns modulo the associative-commutative theory of some constants
$+_1,\ldots, +_n$. Given an AC-unification problem over higher-order
patterns, the output of the algorithm is a finite set DAG solved forms,
constrained by some flexible-flexible equations
with the same head on both sides. Indeed, in the presence of AC
constants, such equations are always solvable, but they have no
minimal complete set of unifiers. We prove that the
algorithm terminates, is sound, and that any solution of the original
unification problem is an instance of one of the computed solutions
which satisfies the constraints.},
PAGES = {267--281}
}
@INPROCEEDINGS{contejean97rta,
AUTHOR = {Evelyne Contejean and Claude March{\'e} and Landy Rabehasaina},
TITLE = {Rewrite systems for natural, integral, and rational
arithmetic},
BOOKTITLE = {8th International Conference on Rewriting Techniques and
Applications},
EDITOR = {Hubert Comon},
PUBLISHER = {Springer},
YEAR = 1997,
MONTH = JUN,
ADDRESS = {Barcelona, Spain},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1232},
FTP = {ftp://ftp.lri.fr/LRI/articles/marche/rta97.ps.gz},
URL = {http://dx.doi.org/10.1007/3-540-62950-5_64},
ABSTRACT = {We give algebraic presentations of the sets of natural numbers,
integers, and rational numbers by convergent rewrite systems which
moreover allow efficient computations of arithmetical expressions. We
then use such systems in the general normalised completion algorithm,
in order to compute Gr\"obner bases of polynomial ideals over % $\Z$ and
${\mathbb{Q}}$.}
}
@TECHREPORT{contejean97rr,
AUTHOR = {Evelyne Contejean and Claude March{\'e} and Landy Rabehasaina},
TITLE = {Rewrite systems for natural, integral, and rational
arithmetic},
INSTITUTION = {Laboratoire de Recherche en Informatique},
YEAR = 1997,
TYPE = {Research Report},
ADDRESS = {Universit{\'e} de Paris-Sud, Orsay, France}
}
@INPROCEEDINGS{boudet96rta,
AUTHOR = {Alexandre Boudet and Evelyne Contejean and Claude
March{\'e}},
TITLE = {{AC}-complete unification and its application to
theorem proving},
BOOKTITLE = {7th International Conference on Rewriting Techniques and
Applications},
EDITOR = {Harald Ganzinger},
PUBLISHER = {Springer},
YEAR = 1996,
MONTH = JUL,
ADDRESS = {New Brunswick, NJ, USA},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1103,
PAGES = {18--32},
FTP = {ftp://ftp.lri.fr/LRI/articles/marche/rta96.ps.gz},
URL = {http://dx.doi.org/10.1007/3-540-61464-8_40},
ABSTRACT = {When one wants to turn a set of equations into a convergent set of
rules by a completion technique, the complexity (and hence efficiency)
of the completion depends directly upon the number of critical pairs
generated, particularly in presence of one or several AC symbols. We
try to reduce this number by use of a new kind of unification
algorithm said \emph{AC-complete}. We show that this new notion of
unification has good properties for our purpose : first it generates smaller
complete sets of unifiers, and second it behaves well (better than
general $E$-unification) with respect to mixing.}
}
@INPROCEEDINGS{contejean96rta,
AUTHOR = {Evelyne Contejean and Claude March{\'e}},
TITLE = {{CiME: Completion Modulo $E$}},
BOOKTITLE = {7th International Conference on Rewriting Techniques and
Applications},
EDITOR = {Harald Ganzinger},
PUBLISHER = {Springer},
YEAR = 1996,
MONTH = JUL,
ADDRESS = {New Brunswick, NJ, USA},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1103,
PAGES = {416--419},
NOTE = {System Description available at \url{http://cime.lri.fr/}},
URL = {http://dx.doi.org/10.1007/3-540-61464-8_70},
FTP = {ftp://ftp.lri.fr/LRI/articles/marche/cime-rta96.ps.gz},
ABSTRACT = {http://www.lri.fr/~marche/cime-rta96.html},
URL = {http://cime.lri.fr/}
}
@INPROCEEDINGS{ajili95cp,
AUTHOR = {Ajili, Farid and Contejean, Evelyne},
TITLE = {Complete Solving of Linear Diophantine Equations and
Inequations without adding Variables},
BOOKTITLE = {Proc. First International Conference on Principles
and Practice of Constraint Programming},
YEAR = 1995,
ADDRESS = {Cassis},
MONTH = SEP,
PAGES = {1--17},
URL = {http://dx.doi.org/10.1007/3-540-60299-2_1},
ABSTRACT = {In this paper, we present an algorithm for solving {\em directly}
linear Diophantine systems of both equations and inequations. Here
directly means without adding slack variables for encoding
inequalities as equalities. This algorithm is an extension of the
algorithm due to Contejean and Devie \cite{contejean94ic} for solving
linear Diophantine systems of equa\-tions, which is itself a
generalization of the algorithm of Fortenbacher for
solving a single linear Diophantine equation. All the nice properties
of the algorithm of Contejean and Devie are still satisfied by the new
algorithm: it is complete, {\em i.e.} provides a (finite) description
of the set of solutions, it can be implemented with a {\em bounded}
stack, and it admits an incremental version. All of these
characteristics enable its easy integration in the CLP paradigm.}
}
@TECHREPORT{ajili95rr,
AUTHOR = {Ajili, F. and Contejean, E.},
TITLE = {Complete solving of linear and Diophantine equational and
inequational systems without adding variables},
INSTITUTION = {INRIA},
YEAR = 1995,
NUMBER = 0175,
MONTH = JUN
}
@ARTICLE{beldiceanu94jmcm,
AUTHOR = {Nicolas Beldiceanu and Evelyne Contejean},
TITLE = {Introducing global constraints in {CHIP}},
JOURNAL = {Journal of {M}athematical and Computer Modelling},
YEAR = 1994,
VOLUME = 20,
NUMBER = 12,
PAGES = {97--123},
FTP = {ftp://ftp.lri.fr/LRI/articles/contejean/jmcm94.ps.gz},
ABSTRACT = {The purpose of this paper is to show how the introduction of new
primitive constraints (e.g. {\em among, diffn, cycle}) over finite
domains in the constraint logic pro\-gram\-ming system CHIP result in
finding very rapidly good solutions for a large class of difficult
sequencing, scheduling, geometrical placement and vehicle routing
problems. The {\em among} cons\-traint allows to specify sequencing
constraints in a very concise way. For the first time, the {\em diffn}
constraint allows to express and to solve directly multidimensional
placement problems where one has to consider non over\-lapping
constraints between $n$-dimensional objects (e.g. rectangles,
pa\-ralle\-le\-pi\-peds). The {\em cycle} constraint makes possible
to specify a wide range of graph partitioning problems that could not
yet be expressed by using current constraint logic pro\-gram\-ming
languages. One of the main advantage of all these new primitives is to
take into account more globally a set of elementary
constraints. Finally, we point out that all the previous primitive
constraints enhance the power of the CHIP system significantly,
allowing to solve real life problems that were not within reach of
constraint technology before.}
}
@ARTICLE{contejean94ic,
AUTHOR = {Evelyne Contejean and Herv{\'e} Devie},
TITLE = {An Efficient Algorithm for Solving Systems of Diophantine
Equations},
JOURNAL = {Information and Computation},
YEAR = 1994,
VOLUME = 113,
NUMBER = 1,
MONTH = AUG,
PAGES = {143--172},
FTP = {ftp://ftp.lri.fr/LRI/articles/contejean/ic94.ps.gz},
ABSTRACT = {In this paper, we describe an algorithm for solving systems of linear
Diophantine equations based on a generalization of an al\-go\-rithm for
solving one equation due to Fortenbacher. It can solve
a system as a whole,
or be used incrementally when the system is a sequential accumulation
of several subsystems. The proof of termination of the algorithm is
difficult, whereas the proofs of com\-ple\-te\-ness and correctness are
straightforward generalizations of For\-ten\-ba\-cher's proof.}
}
@INPROCEEDINGS{boudet94ccl,
AUTHOR = {Alexandre Boudet and Evelyne Contejean},
TITLE = {``{S}yntactic'' {AC}-Unification},
PAGES = {136--151},
BOOKTITLE = {First International Conference on Constraints in
Computational Logics},
EDITOR = {Jean-Pierre Jouannaud},
ADDRESS = {M{\"u}nchen, Germany},
MONTH = SEP,
YEAR = 1994,
SERIES = {Lecture Notes in Computer Science},
VOLUME = 845,
PUBLISHER = {Springer},
FTP = {ftp://ftp.lri.fr/LRI/articles/contejean/ccl94.ps.gz},
ABSTRACT = {The rules for unification in a simple syntactic theory, using
Kirchner's {\em mutation} do not
terminate in the case of associative-commutative theories.
We show that in the case of a linear equation, these rules terminate,
yielding a complete set of solved forms, each variable
introduced by the unifiers corresponding to a (trivial) minimal
solution of the (trivial) Diophantine equation where all coefficients are 1.
A non-linear problem can be first treated as a linear one,
that is considering two occurrences of a same variable as two different variables.
After this step, one has to solve the equations between the different
values that have been obtained for the different occurrences of a same variable.
We show that one can restrict the search of the solutions of these latter equations
to linear substitutions.
This result is based on the analysis of how the minimal solutions of a linear
Diophantine equation
can be built-up using the solutions of the trivial Diophantine equation
associated with the linearized $AC$-equation.
This provides a new $AC$-unification algorithm which does not make an explicit use of the
solving of linear Diophantine equations.}
}
@ARTICLE{contejean93jsc,
AUTHOR = {Evelyne Contejean},
TITLE = {Solving {$*$}-problems modulo Distributivity by a
Reduction to {$AC1$}-unification},
JOURNAL = {Journal of Symbolic Computation},
YEAR = 1993,
VOLUME = 16,
PAGES = {493-521},
FTP = {ftp://ftp.lri.fr/LRI/articles/contejean/jsc93.ps.gz},
ABSTRACT = {We show that unification modulo both-sided
distributivity of the symbol $*$ on $+$ can be reduced to
$AC1$-unification for all unification problems which do not involve
the $+$ operator. Moreover, in this case, we can describe ``almost all''
solutions in a finite way, although there
are in general infinitely many minimal solutions for such problems.}
}
@INPROCEEDINGS{contejean93iclp,
AUTHOR = {Evelyne Contejean},
TITLE = {Solving Linear Diophantine Constraints Incrementally},
EDITOR = {David S. Warren},
SERIES = {Logic Programming},
PAGES = {532--549},
BOOKTITLE = {Proc. of the Tenth Int. Conf. on Logic Programming},
YEAR = 1993,
PUBLISHER = {MIT Press},
ADDRESS = {Budapest, Hungary},
MONTH = JUN,
FTP = {ftp://ftp.lri.fr/LRI/articles/contejean/iclp93.ps.gz},
ABSTRACT = {In this paper, we show how to handle linear Diophantine constraints
in\-cre\-men\-tal\-ly by using several variations of the algorithm by
Contejean and Devie (hereafter called ABCD) for solving linear
Diophantine systems \cite{contejean89},\cite{contejean91}. The basic
algorithm is based on a certain enumeration of the potential solutions
of a system, and termination is ensured by an adequate restriction on
the search. This algorithm generalizes a previous algorithm due to
Fortenbacher, which was restricted to the case of a
single equation. Note that using Fortenbacher's algorithm for solving
systems of Diophantine equations by repeatedly applying it to the
successive equations is completely unrealistic: the tuple of variables
in the solved equation must then be substituted in the rest of the
system by a linear combination of the minimal solutions found in which
the coefficients stand for new variables. Unfortunately, the number
of these minimal solutions is actually exponential in both the number
of variables and the value of the coefficients of the equation solved.
In contrast, ABCD ~solves systems faster, without any intermediate
blow-up, since it considers the system as a whole. Besides, and this
is the new feature described in this paper, it can easily tolerate
additional constraints such as membership constraints, linear
monotonic inequations, and so on. This is due to the enumeration of
tuples which allows a componentwise control of potential solutions.
This is not the case with others (more recent) algorithms for solving
systems of Diophantine equations, which are based on algebraic and
combinatorial techniques.}
}
@INPROCEEDINGS{contejean93icalp,
AUTHOR = {Evelyne Contejean},
TITLE = {A Partial Solution for {D}-unification based on a Reduction
to {AC1}-unification},
PAGES = {621--632},
BOOKTITLE = {20th International Colloquium on
Automata, Languages and Programming},
ADDRESS = {Lund, Sweden},
EDITOR = {Andrzej Lingas and Rolf Karlsson and Svante Carlsson},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {700},
YEAR = 1993,
MONTH = JUL,
FTP = {ftp://ftp.lri.fr/LRI/articles/contejean/icalp93.ps.gz},
ABSTRACT = {We show that deciding unification modulo both-sided
distributivity of a symbol $*$ over a symbol $+$ can be reduced to
$AC1$-unification for all unification problems which do not involve
the $+$ operator. Moreover, we can describe ``almost all'' solutions
in a finite way, although there are in general infinitely many minimal
solutions for such problems. As a consequence, $*$-problems appear as
a good candidate for a notion of solved-form for $D$-unification.}
}
@INPROCEEDINGS{beldiceanu93,
AUTHOR = {Nicolas Beldiceanu and Evelyne Contejean and
Helmut Simonis},
TITLE = {Integrating an algorithm for solving linear constraints
in finite domains in the language {CHIP}},
BOOKTITLE = {Proc. 4th Workshop on Constraint Logic Programming},
MONTH = MAR,
YEAR = 1993,
ABSTRACT = {CHIP is a constraint logic programming language originally designed
and developed at ECRC, and further developed and
marketed by COSYTEC. CHIP is able to solve among other constraints (on
rationals and booleans), linear constraints over finite integer
domains. In this case, its basic mechanism is the combination of
constraint propagation and enumeration of the values in the domain
associated with the given constraints. In this paper we present an
original enumeration method based on an algorithm for solving systems
of linear Diophantine equations due to E. Contejean and H. Devie
\cite{contejean91}. The difficulty is to show that this enumeration
method is compatible with constraint propagation, and that every
solution is computed exactly once.}
}
@INPROCEEDINGS{boudet92alp,
AUTHOR = {Alexandre Boudet and Evelyne Contejean},
TITLE = {On $n$-syntactic equational theories},
PAGES = {446--457},
BOOKTITLE = {3th International Conference on Algebraic and
Logic Programming},
EDITOR = {H{\'e}l{\`e}ne Kirchner and Giorgio Levi},
MONTH = SEP,
YEAR = 1992,
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {632},
ADDRESS = {Volterra, Italy},
ABSTRACT = {We define the $n$-syntactic theories as a natural extension of the syntactic
theories.
A $n$-syntactic theory is an equational theory which admits a finite
presentation in which every proof can be performed with at most $n$
applications of an axiom at the root,but no finite presentation in which
every proof can be performed with at most $n-1$
applications of an axiom at the root.
The $n$-syntactic theories inherit the good properties of the syntactic
theories
for solving the word problem, or matching or unification problems.
We show that for any integer $n\geq 1$, there exists a $n$-syntactic theory.},
FTP = {ftp://ftp.lri.fr/LRI/articles/contejean/alp92.ps.gz}
}
@PHDTHESIS{contejean92these,
AUTHOR = {Evelyne Contejean},
TITLE = {{\'E}l{\'e}ments pour la D{\'e}cidabilit{\'e} de
l'Unification modulo la Distributivit{\'e}},
SCHOOL = {Universit{\'e} Paris-Sud},
YEAR = 1992,
ADDRESS = {Orsay, France},
MONTH = APR,
TYPE = {Th{\`e}se de Doctorat},
ABSTRACT = {Dans cette th\`ese, nous donnons des outils pour
l'unification (ou r\'esolution d'\'equations) modulo la distributivit\'e
(ou modulo $D$)
d'un symbole f sur un symbole g. Cette th\'eorie est l'une des derni\`eres
qui soit d\'eriv\'ee de l'arithm\'etique et pour laquelle il n'est toujours
pas connu si l'unification est d\'ecidable ou non.
Dans une premi\`ere partie, nous \'etudions des probl\`emes particuliers pour
lesquels la d\'ecidabilit\'e est triviale, les probl\`emes \'equilibr\'es
o\`u les termes ne comportent pas de symboles g. Nous d\'ecrivons de
fa\c{c}on pr\'ecise l'ensemble (\'eventuellement infini) des solutions
gr\^ace aux structures, qui poss\`edent une propri\'et\'e de d\'ecomposition
maximale unique vis-\`a-vis d'un op\'erateur $AC1$.
Dans une deuxi\`eme partie, nous introduisons les notions d'indexation et
de stratification qui permettent de donner une caract\'erisation de
l'\'egalit\'e de termes modulo $D$.
Nous utilisons ensuite les propri\'et\'es de la stratification pour
d\'emontrer la
compl\'etude d'un ensemble de r\`egles de transformation, qui r\'eduisent
un probl\`eme \`a un probl\`eme \'equilibr\'e, lequel est ensuite facilement
r\'esolu gr\^ace \`a un passage \`a un probl\`eme modulo $AC1$ dans les
structures. Pur des raisons techniques, nous ne traitons qu'un cas particulier
caract\'eris\'e par une condition d'acyclicit\'e dans un graphe.
Nous d\'ecrivons enfin un algorithme original et efficace de r\'esolution
de syst\`emes lin\'eaires d'\'equations diophantiennes.}
}
@ARTICLE{contejean91,
AUTHOR = {Evelyne Contejean and Herv{\'e} Devie},
TITLE = {R{\'e}solution de syst{\`e}mes lin{\'e}aires
d'{\'e}quations diophantiennes},
JOURNAL = {Comptes-Rendus de l'Acad{\'e}mie des Sciences de Paris},
YEAR = 1991,
VOLUME = 313,
NOTE = {S{\'e}rie I},
PAGES = {115-120},
ABSTRACT = {Nous pr\'esentons ici un algorithme pour r\'esoudre les syst\`emes lin\'eaires
homog\`enes d'\'equations diophantiennes de fa\c{c}on directe, \`a l'aide d'une
interpr\'etation g\'eom\'etrique.}
}
@INPROCEEDINGS{boudet90lics,
AUTHOR = {Alexandre Boudet and Evelyne Contejean and
Herv{\'e} Devie},
TITLE = {A new {AC}-unification algorithm with a new
algorithm for solving diophantine equations},
BOOKTITLE = {Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia},
MONTH = JUN,
YEAR = 1990,
PAGES = {289--299},
PUBLISHER = {IEEE Computer Society Press},
ABSTRACT = {This paper presents a new $AC$-unification algorithm. A new
combination technique for regular collapse-free theories is provided
along the line developped in [Bou Jou Sch 88]. The number of calls to
the diophantine equations solver is bounded by the number of $AC$
symbols times the number of {\em shared variables}. The rest of our
algorithm being linear, this gives a much better idea of how the
complexity of $AC$ unification is related to the complexity of solving
linear diophantine equations. The termination proof is surprisingly
easy, compared to [Fages 84].\\ Finally, systems of constraint linear
diophantine equations can be solved, rather than one equation at a
time, using an algorithm which extends Fortenbacher's algorithm to an
arbitrary dimension. This allows a much more efficient use of the
constraints than in the standard case.
}
}
@INPROCEEDINGS{contejean89,
AUTHOR = {Evelyne Contejean and Herv{\'e} Devie},
TITLE = {Solving systems of linear Diophantine equations},
BOOKTITLE = {Proc. 3rd Workshop on Unification, Lambrecht, Germany},
YEAR = 1989,
MONTH = JUN,
PUBLISHER = {University of Kaiserslautern}
}
@MISC{contejean88,
AUTHOR = {Evelyne Contejean},
TITLE = {Unification associative-commutative},
HOWPUBLISHED = {M{\'e}moire de DEA , Universit{\'e} de Paris Sud, Orsay},
YEAR = 1988
}
This file has been generated by bibtex2html 1.82.