Accueil
Évènements récents
Linking focusing and resolution with selection. ACM Transactions on Computational Logic, 21:18:1-30, 2020. .pdf .bib ACM.
First-order automated reasoning with theories: When deduction modulo theory meets practice. Journal of Automated Reasoning, 64(6):1001-1050, 2020. .pdf ©Springer.
.From Axioms to Rewriting Rules. .pdf Tableau des résultats détaillés par domaines.
.lrat2dk : traduire des certificats SAT en preuves Dedukti (travail en cours).
Présentation
Je suis maître de conférence à l'ENSIIE depuis le premier septembre 2010. Depuis janvier 2016, je suis membre de l'équipe Méthodes du laboratoire Samovar (UMR 5157 CNRS Télécom SudParis).
Je suis également visiteur de l'équipe-projet Inria Deducteam.
Je suis docteur de l'université Henri Poincaré - Nancy 1. Vous pouvez télécharger mon manuscrit de thèse.
J'ai effectué en 2009-2010 un post-doctorat au Max Planck Institut für Informatik dans le groupe de recherche Automation of Logic.
De 2010 à 2015 j'ai fait partie de l'équipe CPR du laboratoire Cédric.
Contacts
On peut me contacter à l'adresse suivante :
ENSIIE1 square de la résistance
91025 Évry cedex
par téléphone au (+33) 01 69 36 73 70, ou par mail à guillaume.burel@ensiie.fr. Utilisez ma clef PGP.
Intérêts en recherche
Mon sujet de thèse portait sur les systèmes de démonstrations ordonnées, notamment à l'aide du cadre des systèmes canoniques abstraits introduit par Claude Kirchner et Nachum Dershowitz, et la simplification des démonstrations via l'intégration du calcul, comme en déduction modulo. Mes intérêts en recherche sont la déduction automatique, la mécanisation du raisonnement, la théorie de la démonstration et la logique en général.
En ce moment, je m'intéresse à la combinaison de théories via la déduction modulo.
J'étais membre de l'Arc Inria Corias qui porte sur la conception d'assistants à la démonstration basés sur la surdéduction modulo.
Voici aussi un lien vers les différents publications et rapports que j'ai rédigés.
Maria Paola Bonacina possède une page sur les systèmes canoniques abstraits.
Enseignements
J'ai été de 2006 à 2009 moniteur à l'université Henri Poincaré. Quelques documents de cours sont disponibles sur ces pages.
Divers
Investissez dans le savon !
Et pourquoi pas un poème :
L'Ulyssado
Je suis le ténébreux qui fit un beau voyage,
Le prince d'Aquitaine, qui conquit la toison.
Ma seule étoile est morte. Plein d'usage et raison,
Porte le soleil noir le reste de ton âge !
Dans la nuit du tombeau de mon petit village,
Rends-moi le Pausilippe ! Et en quelle saison
La fleur qui plaisait tant, dans ma pauvre maison,
Et la treille où le pampre... et beaucoup davantage !
Suis-je Amour ou Phébus ?... Qu'ont bâti mes aïeux ?
Mon front est rouge encore... le front audacieux !
J'ai rêvé dans la grotte où plaît l'ardoise fine.
Et j'ai deux fois vainqueur vu le Tibre latin
Modulant tour à tour sur le mont Palatin
Et soupirs de la sainte, et doulceur angevine.
Gérchim de Nerlay (Claire Grivet)