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

sophie.tourret@mpi-inf.mpg.de

+49-681-9325-2927

 

Physical location:

Campus E1 5, Room 606 (6th floor)

 

surface mail address:

Max-Planck-Institut für Informatik
Saarland Informatics Campus
Building E1 4
66123 Saarbrücken

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