Emmanuel Kounalis

TCS Journal 2004 Journal Article

Sound generalizations in mathematical induction

• Pascal Urso
• Emmanuel Kounalis

Many proofs by induction diverge without a suitable generalization of the goal to be proved. The aim of the present paper is to propose a method that automatically finds a generalized form of the goal before the induction sub-goals are generated and failure begins. The method works in the case of monomorphic theories (see Section 1). However, in contrast to all heuristic-based methods, our generalization method is sound: A goal is an inductive theorem if and only if its generalization is an inductive theorem. As far as we know this is the first approach that proposes sound generalizations for mathematical induction.

ECAI Conference 1992 Conference Paper

A Simplification-Based Approach to Program Synthesis

• Emmanuel Kounalis

LPAR Conference 1992 Conference Paper

SPIKE, an Automatic Theorem Prover

• Adel Bouhoula
• Emmanuel Kounalis
• Michaël Rusinowitch

TCS Journal 1992 Journal Article

Testing for the ground (co-)reducibility property in term-rewriting systems

• Emmanuel Kounalis

Given a term-rewriting system R, a term t is ground-reducible by R if every ground instance tσ of it is R-reducible. A pair (t, s) of terms is ground-co-reducible by R if every ground instance (tσ, sσ] of it for which tσ and sσ are distinct is R-reducible. Ground (co-)reducibility has been proved to be the fundamental tool for mechanizing inductive proofs, together with the Knuth-Bendix completion procedure presented by Jouannaud and Kounalis (1986, 1989). Jouannaud and Kounalis (1986, 1989) also presented an algorithm for testing ground reducibility which is tractable in practical cases but restricted to left-linear term-rewriting systems. The solution of the ground (co-)reducibility problem, for the general case, turned out to be surprisingly complicated. Decidability of ground reducibility for arbitrary term-rewriting systems has been first proved by Plaisted (1985) and independently by Kapur (1987). However, the algorithms of Plaisted and Kapur amount to intractable computation, even in very simple cases. We present here a new algorithm for the general case which outperforms the algorithms of Plaisted and Kapur and even our previous algorithm in case of left-linear term-rewriting systems. We then show how to adapt it to check for ground co-reducibility.

MFCS Conference 1991 Conference Paper

A Solution of the Complement Problem in Associative-Commutative Theories

• Emmanuel Kounalis
• Denis Lugiez
• Loic Pottier

Abstract We show in this paper that the question of checking whether there are ground instances of a term t which are not instances of the terms t1, .. ., tn modulo sets of associativity and commutativity axioms is decidable. This question belongs to the the well-known class of complement problems. Its solution provides a formal basis for automating the process of learning from examples, verifying the sufficient-completeness property of algebraic specifications, designing associative-commutative compilation algorithms, finding solutions of systems of equations and disequations in associative and commutative theories, etc.

AAAI Conference 1990 Conference Paper

Mechanizing Inductive Reasoning

• Emmanuel Kounalis

Automating proofs by induction is important in many computer science and artificial intelligence applications, in particular in program verification and specification systems. We present a new method to prove (and disprove) automatically inductive properties. Given a set of axioms, a well-suited induction scheme is constructed automatically. We call such a scheme a test-set. Then, for proving a property, we just instantiate it with terms from the test-set and apply pure algebraic simplification to the result. This method avoids completion and explicit induction. However it retains their positive features, namely the completeness of the former and t, he robustness of the latter.

MFCS Conference 1990 Conference Paper

Pumping Lemmas for Tree Languages Generated by Rewrite Systems

• Emmanuel Kounalis

Abstract Rewrite systems are directed equations used to compute by repeatedly replacing subterms of a given formula with equal terms until the simplest form possible is obtained. This simplest form is what we call a normal form. The theory of rewriting is in essence a theory of normal forms. Most frequently we are interested in ground normal forms (normal forms without any variables). Since we are only looking at ground terms, the set of ground normal forms of a rewrite system R may be viewed as a formal language generated by R. In this paper we study the language of ground normal forms ( GNFR for short) and give effective algorithms for deciding certain problems about it such as finiteness and representation. To solve these problems pumping lemmas are stated and proved for GNFR. The results we obtain here have a number of direct applications to problems appearing in Inductive theorem proving, Logic programming, Functional programming, Machine Learning, Algebraic specifications, Equational Logic, Communicating processus etc. ..

I&C Journal 1989 Journal Article

Automatic proofs by induction in theories without constructors

• Jean-Pierre Jouannaud
• Emmanuel Kounalis

Inductionless induction consists of using pure equational reasoning for proving the validity of an equation in the initial algebra of a set of equational axioms, which would normally require some kind of induction. Under given hypotheses, the equation is valid iff adding it to the set of axioms does not result in an inconsistency. This inconsistency can be found by the Knuth-Bendix completion algorithm, provided that the signature of the algebra is split into free constructors and defined symbols, which must be completely defined in terms of constructors. This is the base of the so-called inductive completion algorithm of Huet and Hullot. Two key concepts, inductive reducibility and inductive co-reducibility, allow us to extend these techniques in various directions: incomplete specifications, nonfree constructors, no constructors specified, equational term rewriting systems. The method is adapted for proving the consistency property of an enrichment of a specification by new operators and new equations. In addition, we get also a simple algorithm to exhibit a set of constructors of a specification. Finally, inductive co-reducibility is reduced to inductive reducibility and an algorithm for deciding inductive reducibility is given for left linear term rewriting systems.