Guillaume BUREL's Homepage (Guillaume Burel's photo)


Recent topics

Linking focusing and resolution with selection. ACM Transactions on Computational Logic, 21:18:1-30, 2020. .pdf  .bib  ACM.

with Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand et Olivier Hermant. First-order automated reasoning with theories: When deduction modulo theory meets practice. Journal of Automated Reasoning, 64(6):1001-1050, 2020. .pdf  ©Springer.

with Guillaume Rousseau. From Axioms to Rewriting Rules. .pdf  Table with results detailed by domains.

lrat2dk: translating SAT certificates into Dedukti proofs (work in progress).


I am maître de conférence (assistant professor) at the ENSIIE since September 2010. Since January 2016, I am a member of the Methodes team of the Samovar lab (UMR 5157 CNRS Télécom SudParis).

I am also visiting scientist in the Inria project-team Deducteam.

I defended my PhD at the Université Henri Poincaré - Nancy 1. My PhD manuscript is available for download.

I was in 2009-10 a post-doc fellow at the Max Planck Institut für Informatik in the research group Automation of Logic.

From 2010 to 2015, I was part of the CPR team of the Cédric lab.


I can be found at the following address:

1 square de la résistance
91025 Évry cedex

by phone at +33 169 36 73 70, or by email at Please use my PGP key.

Research interests

During my PhD, I have been working on ordered proofs systems, particularly through the framework of the abstract canonical systems, introduced by Claude Kirchner and Nachum Dershowitz, and the simplification of proofs by the integration of computations, as in deduction modulo. I am interested in automated deduction, reasoning mechanization, proof theory and logic in general.

More recently, I am interested in the combination of theories through deduction modulo.

I was a member of the Inria Arc Corias about the conception of proof assistants based on superdeduction modulo.

Here is some link to the different papers I wrote.

Maria Paola Bonacina maintains a page about the abstract canonical systems.


From 2006 to 2009, I was teaching assistant at the Henri Poincaré University. Since 2010, I am assistant professor at ENSIIE. Some lecture notes and related documents are available on this page (in French).


Invest in soap!

Question: If Schrödinger's thought experiment would take place on Mars, would the cat be dead, or alive, or both?

Answer: Dead, because Curiosity killed the cat.