I am a professor at Grenoble INP – Ensimag. I obtained my PhD in 2005 under the supervision of Thierry Boy de la Tour and Ricardo Caferra, and received a PhD award from INPG. I did postdoctoral research at the University of Verona (Italy) under the supervision of Maria Paola Bonacina before being recruited at Ensimag. I defended my Habilitation thesis on Nov. 9th, 2017. The manuscript (in french) is available here.

I am mainly interested in automated reasoning, and have currently been working on:

• Separation logic
• The certification of quantum properties
• The formalization of financial mathematics
• Automated theorem provers for solving SMT problems
• Finite instantiation methods
• Inductive reasoning
• Abductive reasoning

I have recently been interested in the formalization of financial mathematics using the proof assistant Isabelle. A zipped folder containing results about the formalization in Isabelle of the Cox-Ross-Rubinstein model can be found here, though it strongly recommended to get the theory files available on the Archive of Formal Proofs.

Publications

Below is an outdated list of publications. A more complete list is available here.
Journal proceedings

• Mnacho Echenim, Nicolas Peltier and Sophie Tourret. Prime Implicate Generation in Equational Logic. Journal of Artificial Intelligence Research, 2017 (DOI). Paper
• Mnacho Echenim and Nicolas Peltier. A Superposition Calculus for Abductive Reasoning. Journal of Automated Reasoning, 2016. Paper
• Vincent Aravantinos, Mnacho Echenim, and Nicolas Peltier. A resolution calculus for first-order schemata. Fundamenta Informaticae, 125(2):101133, 2013. Paper
• Mnacho Echenim and Nicolas Peltier. Instantiation Schemes for Nested Theories. ACM Transactions on Computational Logic, 14(2):11, 2013. Paper
• Mnacho Echenim and Nicolas Peltier. An instantiation scheme for satisfiability modulo theories. Journal of Automated Reasoning, 48(3), 2012. Paper

Conference and workshop proceedings

• M. Echenim, N. Peltier, and S. Tourret. Quantifier-Free Equational Logic and Prime Implicate Generation. CADE 25, 2015. Paper
• M. Echenim, N. Peltier, and S. Tourret. A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR 2014. Paper
• M. Echenim, N. Peltier, and S. Tourret. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR 2014. Paper
• M. Echenim, N. Peltier, and S. Tourret. An approach to abductive reasoning in equational logic. IJCAI 2013. Extended version

Teaching

I have been co-head of the Financial Engineering department at Ensimag since 2009. These past years, I have been in charge of the following classes:

• Formal Language Theory (Bac + 3). A possibly outdated version of the course notes (in french) is available here.
• Logic bases for Computer Science (Bac + 4). The course notes (in french) are available here. A couple of videos of the lectures (in french) are available below:
  • Resolution – video 1, video 2, video 3
  • Equality – video 1, video 2, video 3, video 4
  • Satisfiability Modulo Theories – video 1, video 2
  • Herbrand’s theorem – video 1, video 2
• Systematic strategies with .NET (Bac + 5)

Conferences on quantum computing

I am in charge of a series of four conferences that serve as an introduction to quantum computing (in french). These conferences are now part of the Kaléidoscope week at Grenoble INP and can be attended by any of the >1700 students of the institute. The conference topics are the following:

• The basis of quantum computing (slides)
• Quantum algorithms (by Alastair Abbott, slides)
• Quantum information (by Mehdi Mhalla, slides)
• Technologies for the design of quantum computers (by Franck Balestro)

Contact Information

Office: LIG, Bâtiment IMAG. 700 avenue Centrale. 38401 St Martin d’Hères. FRANCE
Phone: +33 4 57 42 14 91
Email: Mnacho (dot) Echenim (at) univ-grenoble-alpes (dot) fr