Publications

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.

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 check the soundness of a proof, they lack automation. Regarding automated tools, one still has to be satisfied with their answers Yes/No/Donotknow, 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.

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.

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.

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 R enjoys a property, so does permut R).

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.

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 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.

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.

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ß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.

This paper presents a general method for studying some quotients of the special linear group SL₂ 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₂(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 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.

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 à la Huet, (in particular, the equations of E can be applied 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 λx₁...λx_n.F(x₁,..., x_n)=λx₁...λx_nF(x_σ(1),...,x_σ(n)), where F is a free variable and σ a permutation. This situation requires a slight technical adaptation of the theory.

We present a complete algorithm for the unification of higher-order patterns modulo the associative-commutative theory of some constants +₁,..., +_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.

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öbner bases of polynomial ideals over Q.

In this paper, we present an algorithm for solving 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 [31] 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, i.e. provides a (finite) description of the set of solutions, it can be implemented with a bounded stack, and it admits an incremental version. All of these characteristics enable its easy integration in the CLP paradigm.

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 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.

In this paper, we present an algorithm for solving 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 [31] 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, i.e. provides a (finite) description of the set of solutions, it can be implemented with a bounded stack, and it admits an incremental version. All of these characteristics enable its easy integration in the CLP paradigm.

The rules for unification in a simple syntactic theory, using Kirchner's 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.

In this paper, we describe an algorithm for solving systems of linear Diophantine equations based on a generalization of an algorithm 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 completeness and correctness are straightforward generalizations of Fortenbacher's proof.

The purpose of this paper is to show how the introduction of new primitive constraints (e.g. among, diffn, cycle) over finite domains in the constraint logic programming system CHIP result in finding very rapidly good solutions for a large class of difficult sequencing, scheduling, geometrical placement and vehicle routing problems. The among constraint allows to specify sequencing constraints in a very concise way. For the first time, the diffn constraint allows to express and to solve directly multidimensional placement problems where one has to consider non overlapping constraints between n-dimensional objects (e.g. rectangles, parallelepipeds). The cycle constraint makes possible to specify a wide range of graph partitioning problems that could not yet be expressed by using current constraint logic programming 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.

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.

In this paper, we show how to handle linear Diophantine constraints incrementally by using several variations of the algorithm by Contejean and Devie (hereafter called ABCD) for solving linear Diophantine systems [41],[39]. 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.

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 [39]. The difficulty is to show that this enumeration method is compatible with constraint propagation, and that every solution is computed exactly once.

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.

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>=1, there exists a n-syntactic theory.

Dans cette thèse, nous donnons des outils pour l'unification (ou résolution d'équations) modulo la distributivité (ou modulo D) d'un symbole f sur un symbole g. Cette théorie est l'une des dernières qui soit dérivée de l'arithmétique et pour laquelle il n'est toujours pas connu si l'unification est décidable ou non.

Dans une première partie, nous étudions des problèmes particuliers pour lesquels la décidabilité est triviale, les problèmes équilibrés où les termes ne comportent pas de symboles g. Nous décrivons de façon précise l'ensemble (éventuellement infini) des solutions grâce aux structures, qui possèdent une propriété de décomposition maximale unique vis-à-vis d'un opérateur AC1. Dans une deuxième partie, nous introduisons les notions d'indexation et de stratification qui permettent de donner une caractérisation de l'égalité de termes modulo D. Nous utilisons ensuite les propriétés de la stratification pour démontrer la complétude d'un ensemble de règles de transformation, qui réduisent un problème à un problème équilibré, lequel est ensuite facilement résolu grâce à un passage à un problème modulo AC1 dans les structures. Pur des raisons techniques, nous ne traitons qu'un cas particulier caractérisé par une condition d'acyclicité dans un graphe. Nous décrivons enfin un algorithme original et efficace de résolution de systèmes linéaires d'équations diophantiennes.

Nous présentons ici un algorithme pour résoudre les systèmes linéaires homogènes d'équations diophantiennes de façon directe, à l'aide d'une interprétation géométrique.

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 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.