⋅ ⋅ ⋅ news ⋅ papers ⋅ community ⋅ students ⋅ teaching ⋅ contact ⋅

SOPHIE TOURRET

News

• After seven years of work, I am no longer editor of the AAR newsletter. It is now Julie Cailler's responsibility to spam the AAR world with important news!
• Qi Qiu, Jasmin Blanchette, and I won the CADE 2023 best paper award for “Verified given clause procedures”.
• My first PhD student, Fajar Haifani, successfully defended his PhD thesis in March 2023. His manuscript is here.

Papers

An up-to-date list of my published papers can be found via DBLP or Google scholar. The HAL open science archive should also contain most of my works.

In addition, here is a list of my works, where you can find pdf preprints for closed-access papers (), along with open-access papers (), formal proofs in Isabelle/HOL (), proceedings-free workshop papers (), my theses (), edition works () and draft papers (). It is unlikely that this list will always be up to date. Don't hesitate to contact me if you have trouble obtaining one of my papers.

2024

• A modular formalization of superposition in Isabelle/HOL
  Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret
  ITP 2024: 12:1-12:20
  publisher's page
• HOL Light to Isabelle/HOL translation, rebooted
  Ghilain Bergeron, Stéphane Glondu and Sophie Tourret
  Isabelle workshop 2024
  workshop's page ⋅ author's pdf
• Invited talk: the hows and whys of higher-order SMT
  Sophie Tourret
  SMT@CAV 2024: 1
  workshop's page ⋅ abstract

2023

• Verified given clause procedures
  Jasmin Blanchette, Qi Qiu, and Sophie Tourret
  CADE-29, LNCS 14132, pp. 61–77, Springer
  publisher’s page ⋅ authors’ pdf
• Given clause loops
  Jasmin Blanchette, Qi Qiu and Sophie Tourret
  Archive of Formal Proofs
  AFP entry
• Unifying splitting
  Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret
  J. Autom. Reason. 67(2): 16
  publisher’s page ⋅ authors’ pdf
• Mechanical mathematicians
  Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann
  Communications of the ACM 66(4): 80–90
  publisher’s page ⋅ authors’ pdf
• Complete and efficient higher-order reasoning via lambda-superposition
  Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann
  ACM SIGLOG News 10(4): 25-40
  publisher's page ⋅ authors' pdf
• Superposition for higher-order logic
  Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic
  J. Autom. Reason. 67(1): 10
  publisher's page ⋅ authors' pdf ⋅ errata
  

2022

• A comprehensive framework for saturation theorem proving
  Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette
  J. Autom. Reason. 66(4): 499–539
  publisher’s page ⋅ authors’ pdf
• Making higher-order superposition work
  Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret
  J. Autom. Reason. 66(4): 541–564
  publisher’s page ⋅ authors’ pdf
• A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column
  Sophie Tourret, Christoph Weidenbach
  J. Autom. Reason. 66(4): 575-584
  publisher's page ⋅ authors’ pdf
• Connection-Minimal Abduction in EL via Translation to FOL
  Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
  IJCAR 2022: 188-207
  publisher's page ⋅ arXiv report
• Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract)
  Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
  Description Logics 2022
  publisher's pdf

2021

• Superposition with lambdas
  Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann
  J. Autom. Reason. 65(7): 893–940
  publisher’s page ⋅ arXiv report ⋅ authors’ pdf
• A unifying splitting framework
  Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret
  CADE-28, LNCS 12699, pp. 344–360, Springer
  publisher’s page ⋅ authors’ pdf ⋅ technical report
• Superposition for full higher-order logic
  Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović
  CADE-28, LNCS 12699, pp. 396–412, Springer
  publisher’s page ⋅ authors’ pdf ⋅ technical report ⋅ errata
• Superposition with first-class booleans and inprocessing clausification
  Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic
  CADE-28: 378-395
  publisher’s page ⋅ authors’ pdf ⋅ technical report ⋅ errata
• Making higher-order superposition work
  Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret
  CADE-28, LNCS 12699, pp. 415–432, Springer
  publisher’s page ⋅ authors’ pdf
• Generalized completeness for SOS resolution and its application to a new notion of relevance
  Fajar Haifani, Sophie Tourret, Christoph Weidenbach
  CADE-28: 327-343
  publisher’s page ⋅ authors’ pdf
• A modular Isabelle framework for verifying saturation provers
  Sophie Tourret and Jasmin Blanchette
  CPP 2021, pp. 224–237, ACM
  publisher’s page ⋅ authors’ pdf

2020

• Extensions to the comprehensive framework for saturation theorem proving
  Jasmin Blanchette and Sophie Tourret
  Archive of Formal Proofs
  AFP entry
• A comprehensive framework for saturation theorem proving
  Sophie Tourret
  Archive of Formal Proofs
  AFP entry
• A comprehensive framework for saturation theorem proving
  Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette
  IJCAR 2020, Part I, LNCS 12166, pp. 316–334, Springer
  publisher’s page ⋅ authors’ pdf ⋅ technical report
• Logical reduction of metarules
  Andrew Cropper, Sophie Tourret
  Mach. Learn. 109(7): 1323-1369
  publisher’s page ⋅ arXiv report
• On a Notion of Relevance
  Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
  Description Logics 2020
  publisher's pdf
• Signature-Based Abduction for Expressive Description Logics
  Patrick Koopmann, Warren Del-Pinto, Sophie Tourret, Renate A. Schmidt
  KR 2020: 592-602
  publisher's page ⋅ arXiv report
• Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT
  Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa
  SMT 2020: 3-14
  publisher's page
• Joint proceedings of PAAR and SC-Square 2020, co-located with IJCAR 2020
  Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret (editors)
  CEUR Workshop Proceedings 2752
  proceedings

2019

• Superposition with lambdas
  Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann
  CADE-27, LNCS 11716, pp. 55–73, Springer
  publisher’s page ⋅ authors’ pdf ⋅ technical report
• Stronger higher-order automation: a report on the ongoing Matryoshka project
  Jasmin Blanchette, Pascal Fontaine, Stephan Schulz, Sophie Tourret, and Uwe Waldmann
  ARCADE 2019
  workshop's page ⋅ author's pdf
• SLD-resolution reduction of second-order Horn fragments
  Sophie Tourret, Andrew Cropper
  JELIA 2019: 259-276
  publisher's page ⋅ arXiv report

2018

• Prime implicate generation in equational logic (extended abstract)
  Mnacho Echenim, Nicolas Peltier, Sophie Tourret
  IJCAI 2018: 5588-5592
  publisher's page
• Derivation reduction of metarules in meta-interpretive learning
  Andrew Cropper, Sophie Tourret
  ILP 2018: 1-21
  publisher's page
• SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract
  Sophie Tourret, Andrew Cropper
  TERMGRAPH workshop

2017

• Prime implicate generation in equational logic
  Mnacho Echenim, Nicolas Peltier, Sophie Tourret
  J. Artif. Intell. Res. 60: 827-880
  publisher's page
• Learning logic program representation for delayed systems with limited training data
  Yin Jun Phua, Tony Ribeiro, Sophie Tourret, Katsumi Inoue
  ILP (Late Breaking Papers) 2017: 27-37
  publisher's paper
• Inductive learning from state transitions over continuous domains
  Tony Ribeiro, Sophie Tourret, Maxime Folschette, Morgan Magnin, Domenico Borzacchiello, Francisco Chinesta, Olivier F. Roux, Katsumi Inoue
  ILP 2017: 124-139
  publisher's page
• Learning human-understandable description of dynamical systems from feed-forward neural networks
  Sophie Tourret, Enguerrand Gentet, Katsumi Inoue
  ISNN (1) 2017: 483-492
  publisher's page
• Learning logic program representation from delayed interpretation transition using recurrent neural networks
  Yin Jun Phua, Sophie Tourret, Katsumi Inoue
  SNL workshop
  workshop's page ⋅ author's pdf

2016

• Abduction in first order logic with equality (Prime implicate generation in equational logic)
  Sophie Tourret -- PhD thesis
  Grenoble Alpes University, France
  thesis' pdf
• Learning from interpretation transition using feed-forward neural networks
  Enguerrand Gentet, Sophie Tourret, Katsumi Inoue
  ILP (Short Papers) 2016: 27-33
  publisher's page

2015

• Quantifier-free equational logic and prime implicate generation
  Mnacho Echenim, Nicolas Peltier, Sophie Tourret
  CADE 2015: 311-325
  publisher's page

2014

• A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
  Sophie Tourret, Mnacho Echenim, Nicolas Peltier
  PAAR@IJCAR 2014: 94-104
  publisher's page ⋅ author's pdf
• A superposition-based approach to abductive reasoning in equational clausal logic
  Mnacho Echenim, Nicolas Peltier, Sophie Tourret
  ADDCT workshop
• A Rewriting Strategy to Generate Prime Implicates in Equational Logic
  Mnacho Echenim, Nicolas Peltier, Sophie Tourret
  IJCAR 2014: 137-151
  publisher's page

2013

• An Approach to Abductive Reasoning in Equational Logic
  Mnacho Echenim, Nicolas Peltier, Sophie Tourret
  IJCAI 2013: 531-537
  publisher's page

2012

• A Superposition Strategy for Abductive Reasoning in Ground Equational Logic
  Mnacho Echenim, Nicolas Peltier, Sophie Tourret
  IWS workshop
  author's pdf
• Abduction and Prime Implicates, from Propositional Logic to Equational Logic
  Sophie Tourret -- Master thesis
  Grenoble INP - Ensimag
  thesis' pdf

Community Activities

Program Committees

• PC chair (workshop): PAAR 2020
• PC member: CADE/IJCAR 2021-2023 (CADE x2, IJCAR x1), SBMF 2023, CPP 2022, IJCAI 2018-2024, AAAI 2020, TABLEAU 2019, RW 2019.
• PC member (workshops): LFMTP 2024, PAAR 2020-2024 (x3), SMT 2022-2023, PxTP 2021, SOQE 2021

Steering Committees

• CADE trustee, elected 2022
• PAAR steering committee member, invited 2020

Other contributions to the research community

• Co-organiser of the SAT/SMT/AR summer school 2024
• Editor of the AAR newsletter (2017-2024)
• Workshop chair: CADE 2025, IJCAR 2024, IJCAR 2022
• Publicity chair: CADE 2021

PhD Students

Current

• Martin Desharnais, formalisation of logic, co-supervision with Christoph Weidenbach and Jasmin Blanchette
• Vincent Trélat, enhancement of B language reasoners with SMT techniques, co-supervisen with Stephan Merz

Past

• Fajar Haifani, abduction and relevance in first-order logic and description logics, co-supervision with Christoph Weidenbach

Teaching

• 2022-2024, Secure Coding (with Stephan Merz)
• 2022, Decision Procedures for Proving Programs
• 2020-2021, Decision Procedures for Proving Programs (with Christophe Ringeissen)
• 2019, Concrete Semantics with Isabelle/HOL (with Mathias Fleury)
• 2018-2019, Inductive Logic Programming: a Symbolic Approach to Machine Learning (seminar)
• 2018, Automated Reasoning II (with U. Waldmann)
• 2012-2014, Formal Languages, Databases and Networks (teaching assistant at Grenoble INP - Ensimag).

Contact