RG1
Automation of Logic

Sophie Tourret

 

researcher at Inria, France

guest researcher in the Automation of Logic group at MPII, Germany

Interests

automated reasoning, formal logic, artificial intelligence

Contact

In France (most of the time):

  • stourret@loria.fr
  • +33 354 95 84 78
  • INRIA Nancy & LORIA
    Equipe VeriDis, Bâtiment B
    615, rue du Jardin Botanique
    F-54602 Villers-lès-Nancy
    France
  • LORIA, Room B 208

In Germany (once in a while):

  • stourret@mpi-inf.mpg.de
  • +49-681-9325-2927
  • Max-Planck-Institut für Informatik
    Saarland Informatics Campus
    Building E1 4
    66123 Saarbrücken
    Germany
  • Campus E1 5, Room 606

Teaching

Research topics

My work revolves currently around two projects:

  • Matryoshka, a project that aims at extending state-of-the-art first-order solvers (SMT & Superposition) to higher-order logic. I am involved in the extension of Superposition to HOL, in the developpement of Zipperposition, in the formalisation of a saturation theorem proving framework in Isabelle/HOL and in improving the CCFV-based instantiation scheme of SMT solvers;
  • CPEC (A3), a projects that aims at producing explications in description logics. I have recently started working on using prime implicate generation in first-order logic to produce such explications.

I have also worked on the derivation reduction of second-order Horn fragments.

Information about my previous research topics can be found on:

that correspond to when I was doing my first post-doc and PhD respectively.

Publications

journal papers

  • Logical Reduction of Metarules, Andrew Cropper and Sophie Tourret, MLJ (accepted, to appear), 2019 (arXiv)
  • Prime Implicate Generation in Equational Logic, Mnacho Echenim, Nicolas Peltier, Sophie Tourret, JAIR, 60, 2017 (pdf)

 

conference papers

  • Superposition with Lambdas, Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, and Uwe Waldmann, CADE, 2019 (springer, preprint pdf)
  • SLD-Resolution Reduction of Second-Order Horn Fragments, Sophie Tourret, Andrew Cropper, JELIA, 2019 (springer, preprint pdf, arXiv)
  • Derivation Reduction of Metarules in Meta-interpretive Learning, Andrew Cropper, Sophie Tourret, ILP, 2018 (springer, preprint pdf)
  • Prime Implicate Generation in Equational Logic (extended abstract), Mnacho Echenim, Nicolas Peltier, Sophie Tourret, IJCAI, 2018 (pdf, slides)
  • Extracting Human-Understandable Description of Dynamical Systems from Feed-Forward Neural Networks, Sophie Tourret, Enguerrand Gentet, Katsumi Inoue, ISNN, 2017 (preprint pdf)
  • Learning Logic Program Representation for Delayed Systems with Limited Training Data, Yin Jun Phua, Sophie Tourret, Katsumi Inoue, ILP (short papers), 2017 (preprint pdf)
  • Learning Programs with Continuous Domains from State Transitions, Tony Ribeiro, Sophie Tourret, Maxime Folschette, Morgan Magnin, Domenico Borzacchiello, Francisco Chinesta, Olivier Roux, Katsumi Inoue, ILP, 2017 (preprint pdf)
  • Learning from Interpretation Transition using Feed-Forward Neural Networks, Enguerrand Gentet, Sophie Tourret, Katsumi Inoue, ILP (short papers), 2016 (preprint pdf)
  • Quantifier-Free Equational Logic and Prime Implicate Generation, Mnacho Echenim, Nicolas Peltier, Sophie Tourret, CADE, 2015 (preprint pdf, tech. rep.)
  • A Rewriting Strategy to Generate Prime Implicates in Equational Logic, Mnacho Echenim, Nicolas Peltier, Sophie Tourret, IJCAR, 2014 (preprint pdf)
  • An Approach to Abductive Reasoning in Equational Logic, Mnacho Echenim, Nicolas Peltier, Sophie Tourret, IJCAI, 2013 (preprint pdf, tech. rep.)

 

workshop papers

  • Stronger Higher-Order Automation: A Report on the Ongoing Matryoshka Project, Jasmin Blanchette, Pascal Fontaine, Stephan Schulz, Sophie Tourre, and Uwe Waldmann, ARCADE, 2019 (pdf, slides)
  • SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract, Sophie Tourret, Andrew Cropper, TERMGRAPH, 2018 (slides)
  • Learning Logic Program Representation from Delayed Interpretation Transition Using Recurrent Neural Networks, Yin Jun Phua, Sophie Tourret, Katsumi Inoue, SNL, 2017 (pdf)
  • A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic, Mnacho Echenim, Nicolas Peltier, Sophie Tourret, ADDCT, 2014 (website)
  • A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses, Mnacho Echenim, Nicolas Peltier, Sophie Tourret, PAAR, 2014 (pdf)
  • A Superposition Strategy for Abductive Reasoning in Ground Equational Logic, Mnacho Echenim, Nicolas Peltier, Sophie Tourret, IWS, 2012 (pdf)

 

theses

  • Prime Implicate Generation in Equational Logic, Sophie Tourret, PhD thesis, Grenoble Alpes University, 2016 (pdf)
  • Abduction and Prime Implicates, from Propositional Logic to Equational Logic, Sophie Tourret, Master thesis, Grenoble INP - Ensimag, 2012 (pdf)

Activities

conference-related

 

AAR Newsletter

  • editor of the AAR newsletter (2017-present)

See the schedule for the next issue here.

Awards

Past employment and education