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 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. Lately, I am also applying theorem proving techniques to quantum computing and protocol verification.

News

My PhD student Vincent Trelat received the best paper award at ABZ 2025 for his paper “Encoding B Proof Obligations in SMT-LIB”!
Martin Desharnais successfully defended his PhD thesis in January 2025!

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 (). Papers that received awards are indentified with . 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.

2026

Towards Term-based Verification of Diagrammatic Equivalence
Julie Cailler, Noé Delorme, Simon Perdrix, Sophie Tourret
arXiv: 2602.11035
arXiv page

2025

Formalizing splitting in Isabelle/HOL
Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret
ITP 2025: 22:1-22:19
publisher's page
Compactness Theorem for First-Order Logic
Sophie Tourret and Lawrence C. Paulson
Archive of Formal Proofs
AFP entry
A modular splitting framework for saturation theorem proving
Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret
Archive of Formal Proofs
AFP entry

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
Invited talk: The Spawns of the Saturation Framework
Sophie Tourret
Proceedings of the 7th and 8th Vampire Workshop: 1-6
workshop's page ⋅ extended abstract
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

Project involvement

As a principal investigator

Inria associate team carma, 2024-2026

As a senior collaborator

Blanchette's ERC consolidator grant Nekoka, 2023-2028
French ANR PRCE BLaSST, 2022-2027
ERC COST action EuroProofNet, 2022-2025 (core member, vice leader of WG2 2024-2025)
Blanchette's ERC starting grant Matryoshka, 2017-2022

As a participant

German DFG TCRC CPEC, 2019-2021

Community Activities

Program Committees

PC chair (workshops): LFMTP 2026, Weidenbach60, SMT 2025, PAAR 2020
PC member: CADE/IJCAR 2021-2026 (CADE x3, IJCAR x3), CPP 2022 and 2026, IJCAI 2018-2024, AAAI 2020, TABLEAU 2019, RW 2019.
PC member (national conferences): JFLA 2024, SBMF 2023
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
CADE trustee, elected in 2022, reelected in 2025
PAAR steering committee member, invited in 2020
(past) SMT steering committee, ex-officio member as co-chair of SMT 2025

Other contributions to the research community

Conference chair of CPP 2027 and 2028
CADE and AAR secretary from 2026
Co-organiser of the "deduction" series seminar on Revisiting the Foundations of Deduction in a New World, Dagstuhl seminar 26091
Bill McCune PhD Award committee member, 2024 to 2026
Lecturer at the SAT/SMT/AR summer school 2025
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

Local activities

Scientific integrity correspondent for the centre Inria of Lorraine university
Co-ordaniser of the "Reflexions" seminar 2026

PhD Students

Current

Florent Krasnopol, Automated Theorem Proving over the Reals for Reasoning on Quantum Circuits, co-supervision with Julie Cailler and Stephan Merz
Vincent Trélat, Enhancement of B language reasoners with SMT techniques, co-supervision with Stephan Merz

Past

Martin Desharnais (Ph.D. 2025), Formal Verification of Logical Calculi and Simulations in Isabelle/HOL, co-supervision with Christoph Weidenbach and Jasmin Blanchette
Fajar Haifani (Ph.D. 2023), On a Notion of Abduction and Relevance for First-Order Logic Clause Sets, co-supervision with Christoph Weidenbach

Teaching

2022-2026, 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 équipe VeriDis, bâtiment B 615, rue du Jardin Botanique F-54602 Villers-lès-Nancy France	Max-Planck-Institut für Informatik Saarland Informatics Campus building E1 4 66123 Saarbrücken Germany
	Building Ada Lovelace, office B 208	Campus E1 5, 5th floor
		(only if you know I am there)

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