SOPHIE TOURRET

researcher in automated reasoning at Inria and MPI for Informatics

I am a researcher at the Inria centre at Université de Lorraine in the VeriDis team as well as a guest senior researcher at the Max Planck Institute for Informatics in the Automation of Logic research group.

The current focus of my research is the extension of first-order theorem proving techniques beyond first-order and beyond deduction. In particular, I am interested in higher-order logic and its potential applications for software verification and automation of proof assistants. I am also investigating automated techniques for abduction and their application to proof assistants.

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 (workshops): SMT 2025, 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

SAT/SMT/AR coordination committee member, invited in 2024
EuroProofNet european COST action core member, vice leader of work group 2 on automated theorem provers, invited in 2024
CADE trustee, elected in 2022
PAAR steering committee member, invited in 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

	France (most of the time)	Germany (once in a while)
	sophie.tourretloria.fr	sophie.tourretmpi-inf.mpg.de
	+33 3 54 95 84 78
	centre Inria de l'université de Lorraine	Max-Planck-Institut für Informatik
	équipe VeriDis, bâtiment B	Saarland Informatics Campus
	615, rue du Jardin Botanique	building E1 4
	F-54602 Villers-lès-Nancy	66123 Saarbrücken
	France	Germany
	Building Ada Lovelace, office B 208	Campus E1 5, 5th floor
		(only if you know I am there)

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