Publications

[1]	E. Domenjoud, F. Klay, and Ch. Ringeissen. Combination techniques for non-disjoint equational theories. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy, Lecture Notes in Artificial Intelligence, pages 267-281. Springer Verlag, 1994. [ bib ] Modularity is a central problem in automated deduction in equational theories. The problem may be stated as follows: given two equational theories E1 and E2 and algorithms for solving a problem P in each theory, can one build automatically an algorithm for solving the problem P in E1U E2. Almost all results known up to now are restricted to the case where the signatures of E1 and E2 are disjoint. We consider here the combination of non-disjoint theories, and give sufficient conditions under which algorithms for solving the word problem, the matching problem and the unification problem in the union may be built automatically from algorithms for each theory. The problem is obviously unsolvable in general, and we restrict our attention to theories sharing constructors which have to be defined in a suitable way. We show also that this restriction is however not sufficient in general.
[2]	Ch. Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras (extended version). In A. Voronkov, editor, Proceedings International Conference Logic Programming and Automated Reasoning, St Petersburg (Russia), pages 261-272. Springer Verlag, jul 1992. Lecture Notes in Artificial Intelligence, Subseries of LNCS, 624. [ bib ] We extend the results on combination of disjoint equational theories to combination of equational theories where the only function symbols shared are constants. This is possible because there exist finitely many proper shared terms (the constants) which can be assumed irreducible in any equational proof of the combined theory. We establish a connection between the equational combination framework and a more algebraic one. A unification algorithm provides a symbolic constraint solver in the combination of algebraic structures whose finite domains of values are non disjoint and correspond to constants. Primal algebras are particular finite algebras of practical relevance for manipulating hardware descriptions.
[3]	H. Kirchner and Ch. Ringeissen. A constraint solver in finite algebras and its combination with unification algorithms. In K. Apt, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, Washington (USA), pages 225-239. The MIT Press, nov 1992. [ bib ] In the context of constraint logic programming and theorem proving, the development of constraint solvers on algebraic domains and their combination is of prime interest. A constraint solver in finite algebras is presented for a constraint language including equations, disequations and inequations on finite domains. The method takes advantage of the embedding of a finite algebra in a primal algebra that can be presented, up to an isomorphism, by an equational presentation. We also show how to combine this constraint solver in finite algebras with other unification algorithms, by extending the techniques used for the combination of unification.
[4]	Ch. Ringeissen. Combination of matching algorithms. In P. Enjalbert, E.-W. Mayr, and K.-W. Wagner, editors, Proceedings 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen, volume 775 of Lecture Notes in Computer Science, pages 187-198. Springer Verlag, feb 1994. Extended version available as report 93-R-197. [ bib ] This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint equational theories. The question is under which conditions matching algorithms in the single theories are sufficient to obtain a matching algorithm in the combination? In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms (with linear constant restriction) is always sufficient for solving a pure fragment of combined matching problems. Second, we present a combined matching algorithm which is complete for the largest class of theories where unification is not needed, including collapse-free regular theories and linear theories.
[5]	H. Kirchner and C. Ringeissen. Constraint solving by narrowing in combined algebraic domains. In P. Van Hentenryck, editor, Proceedings International Conference on Logic Programming'94, Santa Margherita (Italy), pages 617-631. MIT Press, jun 1994. [ bib ] Narrowing is a way to integrate function evaluation and equality definition into logic programming. Here we show how this can be combined with the constraint paradigm. We propose a solver for goals with constraints in theories defined by unconstrained equalities and rewrite rules with constraints expressed in an algebraic built-in structure. The narrowing method reduces the goal solving problem in the whole theory to rewriting and constraint solving in an adequate combined theory. The combined solver is obtained through the combination of a solver in the built-in structure and a solver for the unconstrained equalities. Sufficient syntactic conditions are proposed to get a process that enumerates a complete set of solutions.
[6]	H. Kirchner and C. Ringeissen. Combining symbolic constraint solvers on algebraic domains. Journal of Symbolic Computation, 18(2):113-155, Aug 1994. [ bib ] In the context of constraint logic programming and theorem proving, the development of constraint solvers on algebraic domains and their combination is of prime interest. As an example, a constraint solver in finite algebras is presented for a constraint language including for instance equations, disequations and inequations. By extending techniques used for the combination of unification in disjoint equational theories, we show how to combine constraint solvers on different algebraic domains that may share some constant symbols. We illustrate this technique by combining the constraint solver in finite algebras with other unification algorithms, and with another constraint solver on a different finite algebra.
[7]	Christophe Ringeissen. Combining decision algorithms for matching in the union of disjoint equational theories. Information and Computation, 126(2):144-160, May 1996. Journal version of 93-R-249. [ bib ] This paper addresses the problem of systematically building a matching algorithm for the union of two disjoint theories E1 U E2 provided that matching algorithms are known in both theories E1 and E2. In general, the blind use of combination techniques introduces unification. Two different restrictions are considered in order to reduce this unification to matching. First, we show that combining matching algorithms (with linear constant restriction) is always sufficient for solving a pure fragment of combined matching problems. Second, the investigated method is complete for the largest class of theories where unification is not needed, including regular collapse-free theories and linear theories. Syntactic conditions are given to define this class of theories in which solving the combined matching problem is performed in a modular way.
[8]	Christophe Ringeissen. Cooperation of decision procedures for the satisfiability problem. In Frontiers of Combining Systems, First International Workshop, Munich, Germany, Applied Logic, pages 121-140. Kluwer Academic Publishers, mar 1996. Published version of 95-R-233. [ bib ] Constraint programming is strongly based on the use of solvers which are able to check satisfiability of constraints. We show in this paper a rule-based algorithm for solving in a modular way the satisfiability problem w.r.t. a class of theories Th. The case where Th is the union of two disjoint theories Th1 and Th2 is known for a long time but we study here different cases where function symbols are shared by Th1 and Th2. The chosen approach leads to a highly non-deterministic decomposition algorithm but drastically simplifies the understanding of the combination problem. The obtained decomposition algorithm is illustrated by the combination of non-disjoint equational theories.
[9]	Claude Kirchner and Christophe Ringeissen. Higher-order equational unification via explicit substitutions. In K. Meinke M. Hanus, J. Heering, editor, Algebraic and Logic Programming, ALP'97, Southampton, UK, Lecture Notes in Computer Science, pages 61-75. Springer Verlag, sep 1997. [ bib ] We show how to reduce the higher-order E-unification problem into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed Lambda-terms in a first-order setting via a calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and this first-order calculus.
[10]	Christophe Ringeissen. Prototyping combination of unification algorithms with the elan rule-based programming language. In Rewriting Techniques and Applications, RTA'97, Sitges, Spain, Lecture Notes in Computer Science, pages 323-326. Springer Verlag, jun 1997. [ bib ] We present in this system description a rule-based implementation of combination algorithms for the unification problem. This implementation illustrates the ability of the ELAN programming language to prototype constraint solvers.
[11]	Claude Kirchner and Christophe Ringeissen. Rule-based constraint programming. Fundamenta Informaticae, 34(3):225-262, Jun 1998. [ bib ] In this paper we present a view of constraint programming based on the notion of rewriting controlled by strategies. We argue that this concept allows us to describe in a unified way the constraint solving mechanism as well as the meta-language needed to manipulate the constraints. This has the advantage to provide descriptions that are very close to the proof theoretical setting used now to describe constraint manipulations like unification or numerical constraint solving. We examplify the approach by presenting examples of constraint solvers descriptions and combinations written in the elan language.
[12]	Eric Monfroy and Christophe Ringeissen. Solex: a domain-independent scheme for constraint solver extension. In Jacques Calmet and Jan Plaza, editors, International Conference on Artificial Intelligence and Symbolic Computation - AISC'98, Plattsburgh, New York, USA, volume 1476 of Lecture Notes in Artificial Intelligence, pages 222-233. Springer-Verlag, Sep 1998. [ bib ] In declarative programming languages based on the constraint programming paradigm, computations can be viewed as deductions and are enhanced with the use of constraint solvers. However, admissible constraints are restricted to formulae handled by solvers and thus, declarativity may be jeopardized. We present a domain-independent scheme for extending constraint solvers with new function symbols. This mechanism, called Solex, consists of a collaboration of elementary solvers. They add and deduce information related to constraints involving new functions, complete the computation domain and purify constraints. Some extensions of computation domains have already been studied to demonstrate the broad scope of Solex potential applications.
[13]	Peter Borovansky, Salma Jamoussi, Pierre-Etienne Moreau, and Christophe Ringeissen. Handling elan rewrite programs via an exchange format. In Claude Kirchner and Hélène Kirchner, editors, Second Workshop on Rewriting Logic and its Applications - WRLA'98, Pont-à-Moussson, France, volume 15 of Electronic Notes in Theoretical Computer Science. Elsevier Science B. V., 1998. [ bib ] Designing a programming environment raises difficult implementation problems since such software is not just one piece of code able to execute programs expressed in a given programming language, but consists generally of several heterogeneous tools. The idea behind a data exchange format is to provide a common representation for the interconnection of these different tools. Moreover, an exchange format is a way to handle programs like any kind of objects in the programming language, and so it is useful for instance in the context of the reflection problem. In this paper, we report our experiments with the current exchange format created and used by the actual implementation of the rule-based programming language ELAN.
[14]	Peter Borovansky, Claude Kirchner, Hélène Kirchner, Pierre-Etienne Moreau, and Christophe Ringeissen. An overview of elan. In Claude Kirchner and Hélène Kirchner, editors, Second Workshop on Rewriting Logic and its Applications - WRLA'98, Pont-à-Mousson, France, volume 15 of Electronic Notes in Theoretical Computer Science. Elsevier Science B. V., 1998. URL: http://www.elsevier.nl/locate/entcs/volume15.html. [ bib ] This paper presents a comprehensive introduction to the ELAN rule-based programming language. We describe the main features of the language, the ELAN environment, and introduce bibliographic references to various papers addressing foundations, implementation and applications of ELAN.
[15]	Eric Monfroy and Christophe Ringeissen. An open automated framework for constraint solver extension: the solex approach. Fundamenta Informaticae, 39(1-2):167-187, Jul 1999. [ bib ] In declarative programming languages based on the constraint programming paradigm, computations can be viewed as deductions enhanced with the use of constraint solvers. However, admissible constraints are restricted to formulae handled by solvers and thus, declarativity may be jeopardized. We propose a domain-independent scheme to extend constraint solvers so that they can handle alien constraints, i.e., constraint involving new function symbols. This mechanism, called Solex, consists of a set of symbolic rule-based transformations: they add and deduce syntactical as well as semantic information related to alien constraints, complete the computation domain, and purify constraints in order to allow solvers to cope with alien constraints. These transformations can be seen as elementary solvers, and thus, Solex is a collaboration of these several solvers with the initial solver. Some extensions of computation domains have already been studied to demonstrate the broad scope of Solex potential applications.
[16]	Mark G. J. van den Brand and Christophe Ringeissen. Asf+sdf parsing tools applied to elan. In Third International Workshop on Rewriting Logic and Applications - WRLA'2000, Kanazawa, Japon, volume 36. Electronic Notes in Theoretical Computer Science, Sep 2000. [ bib ] This paper describes the development of a new ELAN parser using ASF+SDF parsing technology. ASF+SDF and ELAN are two modern rule-based systems. Both systems have their own features and application domains, however, both formalisms have user-defined syntax for defining rewrite rules. The ASF+SDF Meta-Environment uses powerful and efficient generic parsing tools, whereas the ELAN parser is based on an Earley parser. Furthermore, the ELAN syntax is ``hard-wired'' in the parser, which makes adaptations of the syntax cumbersome. The use of ASF+SDF parsing technology makes the ELAN syntax more open and adaptable, however, some features of the ELAN syntax makes the development of a parser a challenging problem.
[17]	Christophe Ringeissen. Handling relations over finite domains in the rule-based system elan. In Third International Workshop on Rewriting Logic and Applications - WRLA'2000, Kanazawa, Japon, volume 36. Electronic Notes in Theoretical Computer Science, Sep 2000. [ bib ] We present a methodology for handling efficiently relations over small finite domains in the rule-based programming language ELAN. Usually, a relation is specified as a first-order formula (a constraint) interpreted in a given algebraic structure. The concept of rewriting allows us to implement an algebraic structure in a very elegant way, by using rules for defining operators and predicates. Hence, we can directly obtain a rule-based executable specification computing all tuples of a relation, but in most cases, the related computation is completely inefficient. Indeed, the specification of a relation involves conditional rules, and a lot of rewriting steps fail after being tried. In this paper, we use a constraint solver in finite algebras to transform a naive rule-based ELAN specification of a relation into an efficient rule-based ELAN program with only unconditional rules. Thus, the constraint solver enables us to improve the rule-based computation of a relation.
[18]	Christophe Ringeissen and Eric Monfroy. Generating propagation rules for finite domains: a mixed approach. In K. Apt, A. Kakas, E. Monfroy, and F. Rossi, editors, Joint ERCIM/Compulog Net Workshop, Paphos, Cyprus, volume 1865 of Lecture Notes in Artificial Intelligence, pages 150-172. Springer, Oct 2000. [ bib ] Constraint solving techniques are frequently based on constraint propagation, a technique that can be seen as a specific form of deduction. Using constraint programming languages enhanced with constraint handling rules facilities, constraint propagation can be achieved just by applying deduction rules to constraints. The automatic generation of propagation rules has been recently investigated in the particular case of finite domains, when constraint satisfaction problems are based on predefined, explicitly given constraints. Due to its interest for practical applications, several solvers have been developed during the last decade for integrating finite domains into (constraint) logic programming. A possible way of integration is implemented using a unification algorithm to compute most general solutions of constraints. In this paper, we propose a mixed approach for designing finite domain constraints solvers: it consists in using a solver based on unification to improve the generation of propagation rules.
[19]	Hélène Kirchner, Christophe Ringeissen. Frontiers of Combining Systems, volume 1794 of Lecture Notes in Artificial Intelligence, Berlin, Heidelberg, New York, Mar 2000. Springer-Verlag. [ bib ] This volume contains the proceedings of FroCoS'2000, the 3rd International Workshop on Frontiers of Combining Systems, held March 22-24, 2000, in Nancy, France. Like its predecessors organized in Munich (1996) and in Amsterdam (1998), FroCoS'2000 is intended to offer a common forum for research activities related to the combination and the integration of systems in the areas of logic, automated deduction, constraint solving, declarative programming, and artificial intelligence. The topics covered by the selected papers include: combination of logics; combination of constraint solving techniques, combination of decision procedures; modular properties for theorem proving; combination of deduction systems and computer algebra; integration of decision procedures and other solving processes into constraint programming and deduction systems.
[20]	Christophe Ringeissen. Matching with free function symbols - a simple extension of matching? In Aart Middeldorp, editor, International Conference on Rewriting Techniques and Applications - RTA'2001, Utrecht, The Netherlands, volume 2051 of Lecture Notes in Computer Science, pages 276-290. Vincent van Oostrom, Springer-Verlag, May 2001. [ bib ] Matching is a solving process which is crucial in declarative (rule-based) programming languages. In order to apply rules, one has to match the left-hand side of a rule with the term to be rewritten. In several declarative programming languages, programs involve operators that may also satisfy some structural axioms. Therefore, their evaluation mechanism must implement powerful matching algorithms working modulo equational theories. In this paper, we show the existence of an equational theory where matching is decidable (resp. finitary) but matching in presence of additional (free) operators is undecidable (resp. infinitary). The interest of this result is to easily prove the existence of a frontier between matching and matching with free operators.
[21]	Pierre-Etienne Moreau, Christophe Ringeissen, and Marian Vittek. A pattern-matching compiler. In Mark van den Brand and Didier Parigot, editors, First Workshop on Language Descriptions, Tools and Applications - LDTA'01, Genova, Italy, volume 44-2 of Electronic Notes in Theoretical Computer Science. Elsevier, Apr 2001. [ bib ] Implementation of a rule-based transformation engine consists of several tasks with various abstraction levels. We present a new tool called MTOM for the efficient implementation of rule-based transformations. This engine should help to bridge the gap between rewriting implementations and practical applications. It aims at implementing well-identified parts of complex applications where the use of rewriting is natural or crucial. These parts are specified using rewrite rules and integrated with the rest of the application, which is kept in a classical imperative language such as C, C++ or Java. Our tool, which can be viewed as a YACC-like pre-processor, does not depend on a given term representation, rather it accepts implementation of terms (or term like data-types) of yet existing applications and it permits to define and execute rewrite rules upon those types. From our experiences, this system is well-suited for industrial use as well as for implementations of rule-based languages. The paper introduces several features supported by MTOM.
[22]	Peter Borovansky, Claude Kirchner, Hélène Kirchner, and Christophe Ringeissen. Rewriting with strategies in elan: a functional semantics. International Journal of Foundations of Computer Science, 12(1):69-95, Feb 2001. [ bib ] In this work, we consider term rewriting from a functional point of view. A rewrite rule is a function that can be applied to a term using an explicit application function. From this starting point, we show how to build more elaborated functions, describing first rewrite derivations, then sets of derivations. These functions, that we call strategies, can themselves be defined by rewrite rules and the construction can be iterated leading to higher-order strategies. Furthermore, the application function is itself defined using rewriting in the same spirit. We present this calculus and study its properties. Its implementation in the ELAN language is used to motivate and exemplify the whole approach. The expressiveness of ELAN is illustrated by examples of polymorphic functions and strategies.
[23]	David Déharbe, Anamaria Martins Moreira, and Christophe Ringeissen. Improving symbolic model checking by rewriting temporal logic formulae. In Sophie Tison, editor, International Conference on Rewriting Techniques and Applications - RTA'2002, Copenhagen, Denmark, volume 2378 of Lecture Notes in Computer Science, pages 207-221. Thomas Arts, Springer-Verlag, Jul 2002. [ bib ] A factor in the complexity of conventional algorithms for model checking Computation Tree Logic (CTL) is the size of the formulae, and, more precisely, the number of fixpoint operators. This paper addresses the following questions: given a CTL formula, is there an equivalent formula with fewer fixpoint operators? and how term rewriting techniques may be used to find it? Moreover, for some sublogics of CTL, e.g. the sub-logic NFCTL (no fixpoint computation tree logic), more efficient verification procedures are available. This paper also addresses the problem of testing whether an expression belongs or not to NFCTL, and providing support in the choice of the most efficient amongst different available verification algorithms. In this direction, we propose a rewrite system modulo AC, and discuss its implementation in ELAN, showing how this rewriting process can be plugged in a formal verification tool.
[24]	Hélène Kirchner and Christophe Ringeissen, editors. Algebraic Methodology And Software Technology, volume 2422 of Lecture Notes in Computer Science. Springer-Verlag, Sep 2002. [ bib ] This book constitutes the refereed proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002, held in Saint-Gilles-les-Bains, Reunion Island, France in September 2002. The 26 revised full papers presented together with 6 invited papers and 2 system descriptions were carefully reviewed and selected from 59 submissions.
[25]	Mark G. J. van den Brand, Pierre-Etienne Moreau, and Christophe Ringeissen. The elan environment: an rewriting logic environment based on asf+sdf technology. In Workshop on Language Descriptions, Tools and Applications - LDTA'02, Grenoble, France, volume 65 of Electronic Notes in Theoretical Computer Science, Apr 2002. [ bib ] This paper describes the development of a new ELAN environment using ASF+SDF meta-environment component technology. The ELAN environment is an interactive environment for the construction of algebraic specifications. The architecture of this new ELAN environment is inspired by the architecture of the ASF+SDF meta-environment, which is an interactive development environment for the automatic generation of interactive systems for constructing language definitions and generating tools for them. The use of ASF+SDF meta environment component technology makes the ELAN environment more open, adaptable, and reusable.
[26]	Christophe Ringeissen. Matching in a class of combined non-disjoint theories. In Franz Baader, editor, 19th International Conference on Automated Deduction - CADE'2003, Miami, Floride, USA, volume 2741 of Lecture Notes in Artificial Intelligence, pages 212-227. Geoff Sutcliffe, Springer-Verlag, Aug 2003. [ bib ] Solving equational problems is an ubiquitous process in automated deduction, where one needs for instance unification in completion procedures to compute critical pairs, and matching to apply rewrite rules. We present new equational matching and unification results in some combinations of non-disjoint equational theories. Some results are already known for theories sharing an appropriate notion of constructors. We investigate the idea of considering theories that are not explicitly based on the notion of constructors. In this direction, a new class of theories is presented, where a theory is defined as a union of two subtheories, one such that shared symbols do not affect the behavior of the theory, and another one given by a term rewrite system on shared symbols. Matching and unification problems are studied for this class of theories, and for unions of theories in this class. Results obtained for the matching problem are particularly relevant.
[27]	Anamaria Martins-Moreira, Christophe Ringeissen, and Anderson Santana. A tool support for reusing elan rule-based components. In Pierre-Etienne Moreau Jean-Louis Giavitto, editor, 4th International Workshop on Rule-Based Programming - RULE'2003, Valence, Espagne, volume 86 of Electronic Notes in Theoretical Computer Science. Jean-Louis Giavitto, Pierre-Etienne Moreau, Elsevier, Sep 2003. [ bib ] The adaptation of software components developed for a specific application in order to generate reusable components often includes some kind of generalization. This generalization may be carried out, for instance, by the renaming of some identifiers or by its parameterization. In our work, we are specially interested in the generalization by parameterization of algebraic specification components. Generalization and some other transformations on algebraic specifications are being integrated in the FERUS tool. This tool was initially developed for the Common Algebraic Specification Language, called CASL, and we show in the paper its adaptation to the new version of the rule-based programming language ELAN.
[28]	Pierre-Etienne Moreau, Christophe Ringeissen, and Marian Vittek. A pattern matching compiler for multiple target languages. In Görel Hedin, editor, International Conference on Compiler Construction - CC'2003, Varsovie, Pologne, volume 2622 of Lecture notes in Computer Science, pages 61-76, Apr 2003. [ bib ] Many processes can be seen as transformations of tree-like data structures. In compiler construction, for example, we continuously manipulate trees and perform tree transformations. This paper introduces a pattern matching compiler (TOM): a set of primitives which add pattern matching facilities to imperative languages such as C, Java, or Eiffel. We show that this tool is extremely non-intrusive, lightweight and useful to implement tree transformations. It is also flexible enough to allow the reuse of existing data structures.
[29]	Cesare Tinelli and Christophe Ringeissen. Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science, 290(1):291-353, Jan 2003. [ bib ] In this paper we outline a theoretical framework for the combination of decision procedures for constraint satisfiability. We describe a general combination method which, given a procedure that decides constraint satisfiability with respect to a constraint theory T1 and one that decides constraint satisfiability with respect to a constraint theory T2, produces a procedure that (semi-)decides constraint satisfiability with respect to the union of T1 and T2. We provide a number of model-theoretic conditions on the constraint language and the component constraint theories for the method to be sound and complete, with special emphasis on the case in which the signatures of the component theories are non-disjoint. We also describe some general classes of theories to which our combination results apply, and relate our approach to some of the existing combination methods in the field.