I am an associate professor (HDR) 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:

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

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.


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


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:
  • Introduction to the .NET platform (Bac + 5)

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

Featuring WPMU Bloglist Widget by YD WordPress Developer