`Travelled to:`

1 × Estonia

1 × France

1 × Hungary

1 × Italy

1 × Serbia

1 × Sweden

1 × The Netherlands

2 × Spain

2 × USA

2 × United Kingdom

4 × Germany

`Collaborated with:`

A.Boudet ∅ C.Marché S.Conchon P.Corbineau M.Iguernelala P.Courtieu J.Forest O.Pons X.Urbain V.Benzaken S.Dumbrava A.Coste B.Monate L.Rabehasaina H.Devie J.Kanig S.Lescuyer A.Paskevich F.Bobot A.Mahboubi A.Mebsout G.Melquiond

`Talks about:`

unif (5) algorithm (4) rewrit (4) complet (3) certifi (3) theori (3) system (3) proof (3) equat (3) solv (3)

## Person: Evelyne Contejean

### DBLP: Contejean:Evelyne

### Contributed to:

### Wrote 18 papers:

- ESOP-2014-BenzakenCD #coq #formal method #relational
- A Coq Formalization of the Relational Data Model (VB, EC, SD), pp. 189–208.
- IJCAR-2012-BobotCCIMMM #integer #linear
- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic (FB, SC, EC, MI, AM, AM, GM), pp. 67–81.
- RTA-2011-ContejeanCFPU #automation #proving
- Automated Certified Proofs with CiME3 (EC, PC, JF, OP, XU), pp. 21–30.
- TACAS-2011-ConchonCI #modulo theories
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories (SC, EC, MI), pp. 45–59.
- PEPM-2010-ContejeanPUCPF #approach #automation #proving #termination
- A3PAT, an approach for certified automated termination proofs (EC, AP, XU, PC, OP, JF), pp. 63–72.
- SMT-2007-ConchonCKL08 #congruence #semantics
- CC(X): Semantic Combination of Congruence Closure with Solvable Theories (SC, EC, JK, SL), pp. 51–69.
- CADE-2005-ContejeanC #first-order #logic #proving #similarity
- Reflecting Proofs in First-Order Logic with Equality (EC, PC), pp. 7–22.
- RTA-2004-Contejean #algorithm
- A Certified AC Matching Algorithm (EC), pp. 70–84.
- RTA-2001-BoudetC #algorithm
- Combining Pattern E-Unification Algorithms (AB, EC), pp. 63–76.
- RTA-2000-ContejeanCM #physics
- Rewriting Techniques in Theoretical Physics (EC, AC, BM), pp. 80–94.
- CADE-1998-BoudetC #confluence #equation #term rewriting
- About the Confluence of Equational Pattern Rewrite Systems (AB, EC), pp. 88–102.
- RTA-1997-ContejeanMR #term rewriting
- Rewrite Systems for Natural, Integral, and Rational Arithmetic (EC, CM, LR), pp. 98–112.
- RTA-1996-BoudetCM #proving #theorem proving #unification
- AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.
- RTA-1996-ContejeanM #named
- C
*i*ME: Complet*i*on Modulo*E*(EC, CM), pp. 416–419. - ICALP-1993-Contejean #reduction
- A Partial Solution for D-Unification Based on a Reduction to AC1-Unification (EC), pp. 621–632.
- ICLP-1993-Contejean #constraints #incremental #linear
- Solving Linear Diophantine Constraints Incrementally (EC), pp. 532–549.
- ALP-1992-BoudetC #equation #on the
- On n-Syntactic Equational Theories (AB, EC), pp. 446–457.
- LICS-1990-BoudetCD #algorithm #equation #unification
- A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations (AB, EC, HD), pp. 289–299.