Completeness in Data Type Specifications. - Emmanuel Kounalis (European Conference on Computer Algebra (2), 1985)

Proofs by induction in equational theories without constructors. - Jean-Pierre Jouannaud; Emmanuel Kounalis (Bull. EATCS, 1985)

Automatic Proofs by Induction in Equational Theories Without Constructors - Jean-Pierre Jouannaud; Emmanuel Kounalis (LICS, 1986)

Automatic Proofs by Induction in Theories without Constructors - Jean-Pierre Jouannaud; Emmanuel Kounalis (Inf. Comput., 1989)

Testing for Inductive (Co)-Reducibility. - Emmanuel Kounalis (CAAP, 1990)

A Proof System for Conditional Algebraic Specifications. - Emmanuel Kounalis; Michaël Rusinowitch (CTRS, 1990)

Learning from examples and counterexamples with equational background knowledge. - Emmanuel Kounalis (TAI, 1990)

Pumping Lemmas for Tree Languages Generated by Rewrite Systems. - Emmanuel Kounalis (MFCS, 1990)

Mechanizing inductive reasoning. - Emmanuel Kounalis; Michaël Rusinowitch (Bull. EATCS, 1990)

Studies on the Ground Convergence Property of Conditional Theories. - Emmanuel Kounalis; Michaël Rusinowitch (AMAST, 1991)

Automatic Proof Methods for Algebraic Specifications. - Emmanuel Kounalis; Michaël Rusinowitch (FCT, 1991)

A Solution of the Complement Problem in Associative-Commutative Theories. - Emmanuel Kounalis; Denis Lugiez; Loic Pottier (MFCS, 1991)

Compilation of Pattern Matching with Associative-Commutative Functions. - Emmanuel Kounalis; Denis Lugiez (TAPSOFT, Vol.1, 1991)

On Word Problems in Horn Theories. - Emmanuel Kounalis; Michaël Rusinowitch (J. Symb. Comput., 1991)

A Simplification-Based Approach to Program Synthesis. - Emmanuel Kounalis (ECAI, 1992)

SPIKE, an Automatic Theorem Prover. - Adel Bouhoula; Emmanuel Kounalis; Michaël Rusinowitch (LPAR, 1992)

Learning from Examples in Universe of Discourse Described by a Set of equations. - Emmanuel Kounalis (Int. J. Artif. Intell. Tools, 1992)

Testing for the Ground (Co-)Reducibility Property in Term-Rewriting Systems. - Emmanuel Kounalis (Theor. Comput. Sci., 1992)

A Logical Framework for Concept Learning with Background Knowledge. - Emmanuel Kounalis; Michaël Rusinowitch (Int. J. Artif. Intell. Tools, 1993)

Mechanizable Inductive Proofs for a Class of Forall Exists Formulas. - Jacques Chazarain; Emmanuel Kounalis (CADE, 1994)

Reasoning with Conditional Axioms. - Emmanuel Kounalis; Michaël Rusinowitch (Ann. Math. Artif. Intell., 1995)

Automated Mathematical Induction. - Adel Bouhoula; Emmanuel Kounalis; Michaël Rusinowitch (J. Log. Comput., 1995)

Generalization Discovery for Proofs by Induction in Conditional Theories. - Emmanuel Kounalis; Pascal Urso (FLAIRS, 1999)

Mechanizing Proofs of Integrity Constraints in the Situation Calculus. - Emmanuel Kounalis; Pascal Urso (IEA/AIE, 1999)

Automatic Proofs of Properties of Simple C- Modules. - Carine Fédèle; Emmanuel Kounalis (ASE, 1999)

Généralisations correctes pour l'induction mathématique. - Pascal Urso; Emmanuel Kounalis (JFPLC, 2002)

"Term Partition" for Mathematical Induction. - Pascal Urso; Emmanuel Kounalis (RTA, 2003)

Sound generalizations in mathematical induction. - Pascal Urso; Emmanuel Kounalis (Theor. Comput. Sci., 2004)

Rewriting of imperative programs into logical equations. - Olivier Ponsini; Carine Fédèle; Emmanuel Kounalis (Sci. Comput. Program., 2005)