Page de Guillaume BUREL (photo de Guillaume Burel)

Publications

Manuscrits soumis/non publiés

New ! Guillaume Burel. Cut Admissibility by Saturation. .pdf

Guillaume Burel. From Axioms to Rewriting Rules. .pdf  Accès aux ressources mentionnées dans l'article.

Paul Brauner, Guillaume Burel, Gilles Dowek and Benjamin Wack. Normalization in Supernatural deduction and in Deduction modulo , 2010. .pdf 

Acceptées (Journaux et conférences)

Guillaume Burel et Simon Cruanes. Detection of first-order axiomatic theories. In Pascal Fontaine, Christophe Ringeissen et Renate Schmidt (dir.), FroCoS, volume 8152 de LNAI, pages 229-244. Springer, 2013. .pdf  .bib  ©Springer.Abstract Automated theorem provers for first-order logic with equality have become very powerful and useful, thanks to both advanced calculi - such as superposition and its refinements - and mature implementation techniques. Nevertheless, dealing with some axiomatic theories remains a challenge because it gives rise to a search space explosion. Most attempts to deal with this problem have focused on specific theories, like AC (associative commutative symbols) or ACU (AC with neutral element). Even detecting the presence of a theory in a problem is generally solved in an ad-hoc fashion. We present here a generic way of describing and recognizing axiomatic theories in clausal form first-order logic with equality. Subsequently, we show some use cases for it, including a redundancy criterion that can be applied to some equational theories, extending some work that has been done by Avenhaus, Hillenbrand and Löchner.

Guillaume Burel. Experimenting with deduction modulo. In Viorica Sofronie-Stokkermans et Nikolaj Bjørner (dir.), CADE, volume 6803 de LNCS, pages 162-176. Springer, 2011. .pdf  .bib  ©Springer.Abstract Deduction modulo is a generic framework to describe proofs in a theory better than using raw axioms. This is done by presenting the theory through rules rewriting terms and propositions. In CSL 2010, LNCS 6247, p.155-169, we gave theoretical justifications why it is possible to embed a proof search method based on deduction modulo, namely Ordered Polarized Resolution Modulo, into an existing prover. Here, we describe the implementation of these ideas, starting from iProver. We test it by confronting Ordered Polarized Resolution Modulo and other proof-search calculi, using benchmarks extracted from the TPTP Library. For the integration of rewriting, we also compare several implementation techniques, based for instance on discrimination trees or on compilation. These results reveal that deduction modulo is a promising approach to handle proof search in theories in a generic but efficient way.

Guillaume Burel. Efficiently simulating higher-order arithmetic by a first-order theory modulo. Logical Methods in Computer Science, 7(1:3):1-31, 2011. .pdf, LMCS-online.Abstract In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems—such as for instance natural deduction—are applied. Therefore, the reasoning that is intrinsic of the theory does not appear in the length of proofs. In general, the congruence is defined through a rewrite system over terms and propositions. We define a rigorous framework to study proof lengths in deduction modulo, where the congruence must be computed in polynomial time. We show that even very simple rewrite systems lead to arbitrary proof-length speed-ups in deduction modulo, compared to using axioms. As higher-order logic can be encoded as a first-order theory in deduction modulo, we also study how to reinterpret, thanks to deduction modulo, the speed-ups between higher-order and first-order arithmetics that were stated by Gödel. We define a first-order rewrite system with a congruence decidable in polynomial time such that proofs of higher-order arithmetic can be linearly translated into first-order arithmetic modulo that system. We also present the whole higher-order arithmetic as a first-order system without resorting to any axiom, where proofs have the same length as in the axiomatic presentation.

Guillaume Burel. Embedding deduction modulo into a prover. In Anuj Dawar et Helmut Veith (dir.), CSL, volume 6247 de LNCS, pages 155-169. Springer, 2010. .pdf  .bib  ©Springer.Abstract Deduction modulo consists in presenting a theory through rewrite rules to support automatic and interactive proof search. It induces proof search methods based on narrowing, such as the polarized resolution modulo. We show how to combine this method with more traditional ordering restrictions. Interestingly, no compatibility between the rewriting and the ordering is requested to ensure completeness. We also show that some simplification rules, such as strict subsumption eliminations and demodulations, preserve completeness. For this purpose, we use a new framework based on a proof ordering. These results show that polarized resolution modulo can be integrated into existing provers, where these restrictions and simplifications are present. We also discuss how this integration can actually be done by diverting the main algorithm of state-of-the-art provers.

Guillaume Burel et Claude Kirchner. Regaining cut admissibility in deduction modulo using abstract completion. Information and Computation, 208(2):140-164, 2010. .pdf  .bib  ©Elsevier.Abstract Deduction modulo is a way to combine computation and deduction in proofs, by applying the inference rules of a deductive system (e.g. natural deduction or sequent calculus) modulo some congruence that we assume here to be presented by a set of rewrite rules. Using deduction modulo is equivalent to proving in a theory corresponding to the rewrite rules, and leads to proofs that are often shorter and more readable. However, cuts may be not admissible anymore.
We define a new system, the unfolding sequent calculus, and prove its equivalence with the sequent calculus modulo, especially w.r.t. cut-free proofs. It permits to show that it is even undecidable to know if cuts can be eliminated in the sequent calculus modulo a given rewrite system.
Then, to recover the cut admissibility, we propose a procedure to complete the rewrite system such that the sequent calculus modulo the resulting system admits cuts. This is done by generalizing the Knuth-Bendix completion in a non-trivial way, using the framework of abstract canonical systems.
These results enlighten the entanglement between computation and deduction, and the power of abstract completion procedures. They also provide an effective way to obtain systems admitting cuts, therefore extending the applicability of deduction modulo in automated theorem proving.

Guillaume Burel. Automating theories in intuitionistic logic. In Silvio Ghilardi et Roberto Sebastiani (dir.), FroCoS, volume 5749 de LNAI, pages 181-197. Springer, 2009. .pdf  .bib  ©Springer.Abstract Deduction modulo consists in applying the inference rules of a deductive system modulo a rewrite system over terms and formulae. This is equivalent to proving within a so-called compatible theory. Conversely, given a first-order theory, one may want to internalize it into a rewrite system that can be used in deduction modulo, in order to get an analytic deductive system for that theory. In a recent paper, we have shown how this can be done in classical logic. In intuitionistic logic, however, we show here not only that this may be impossible, but also that the set of theories that can be transformed into a rewrite system with an analytic sequent calculus modulo is not co-recursively enumerable. We nonetheless propose a procedure to transform a large class of theories into compatible rewrite systems. We then extend this class by working in conservative extensions, in particular using Skolemization.

Guillaume Burel. Bonnes démonstrations en déduction modulo. Thèse de doctorat, Université Henri Poincaré (Nancy 1), 2009. .pdf .bib TELAbstract Cette thèse étudie comment l'intégration du calcul dans les démonstrations peut les simplifier. Nous nous intéressons pour cela à la déduction modulo et à la surdéduction, deux formalismes proches dans lesquels le calcul est incorporé dans les démonstrations via un système de réécriture. Pour améliorer la recherche mécanisée de démonstration, nous considérons trois critères de simplicité.
L'admissibilité des coupures permet de restreindre l'espace de recherche des démonstrations, mais elle n'est pas toujours assurée en déduction modulo. Nous définissons une procédure qui complète le système de réécriture pour, au final, admettre les coupures. Au passage, nous montrons comment transformer toute théorie pour l'intégrer à la partie calculatoire des démonstrations.
Nous montrons ensuite comment la déduction modulo permet de réduire arbitrairement la taille des démonstrations, en transférant des étapes de déduction dans le calcul. En particulier, nous appliquons ceci à l'arithmétique d'ordre supérieur pour démontrer que les réductions de taille qui sont possibles en augmentant l'ordre dans lequel on se place disparaissent si on travaille en déduction modulo.
Suite à ce dernier résultat, nous avons recherchés quels sont les systèmes d'ordre supérieur pouvant être simulés au premier ordre, en déduction modulo. Nous nous sommes intéressés aux systèmes de type purs et nous montrons comment ils peuvent être encodés en surdéduction, ce qui offre de nouvelles perspectives concernant leur normalisation et la recherche de démonstration dans ceux-ci. Nous développons également une méthodologie qui permet d'utiliser la surdéduction pour spécifier des systèmes de déduction.

Guillaume Burel. A first-order representation of pure type systems using superdeduction. In Frank Pfenning (dir.), LICS, pages 253-263. IEEE Computer Society, 2008. .pdf .bib ©IEEEAbstract Superdeduction is a formalism closely related to deduction modulo which permits to enrich a first-order deduction system---such as natural deduction or sequent calculus---with new inference rules automatically computed from the presentation of a theory. We give a natural encoding from every Pure Type System (PTS) into superdeduction by defining an appropriate first-order theory. We prove that this translation is correct and conservative, showing a correspondence between valid typing judgment in the PTS and provable sequents in the corresponding superdeductive system. As a byproduct, we also introduce the superdeductive sequent calculus for intuitionistic logic, which was until now only defined for classical logic. We show its equivalence with the superdeductive natural deduction. We also prove that for a large class of theories, the newly created rules suffice to show all results related to the theory only. These results lead to a better understanding of the implementation and the automation of proof search for PTS, as well as to more cooperation between proof assistants.

Guillaume Burel. Unbounded proof-length speed-up in deduction modulo. In Jacques Duparc et Thomas Henziger (dir.), CSL, volume 4646 de LNCS, pages 496-511. Springer, 2007. .pdf  .tex  .bib  ©Springer, see also a more advanced version.Abstract In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37 years before: there exist arithmetical formulas that are provable in first order arithmetic, but whose shorter proof in second order arithmetic is arbitrarily smaller than any proof in first order. On the other hand, resolution for higher order logic can be simulated step by step in a first order narrowing and resolution method based on deduction modulo, whose paradigm is to separate deduction and computation to make proofs clearer and shorter. We prove that i + 1-th order arithmetic can be linearly simulated into i-th order arithmetic modulo some confluent and terminating rewrite system. We also show that there exists a speed-up between i-th order arithmetic modulo this system and i-th order arithmetic without modulo. All this allows us to prove that the speed-up conjectured by Gödel does not come from the deductive part of the proofs, but can be expressed as simple computation, therefore justifying the use of deduction modulo as an efficient first order setting simulating higher order.

Guillaume Burel et Claude Kirchner. Cut elimination in deduction modulo by abstract completion. In Sergei N. Artemov et Anil Nerode (dir.), LFCS, volume 4514 de LNCS, pages 115-131. Springer, 2007. .pdf  .tex  .bib  ©Springer.Abstract Deduction Modulo implements Poincaré's principle by identifying deduction and computation as different paradigms and making their interaction possible. This leads to logical systems like the sequent calculus or natural deduction modulo. Even if deduction modulo is logically equivalent to first-order logic, proofs in such systems are quite different and dramatically simpler with one cost: cut elimination may not hold anymore. We prove first that it is even undecidable to know, given a congruence over propositions, if cuts can be eliminated in the sequent calculus modulo this congruence. Second, to recover the cut admissibility, we show how computation rules can be added following the classical idea of completion a la Knuth and Bendix. Because in deduction modulo, rewriting acts on terms as well as on propositions, the ob jects are much more elaborated than for standard completion. Under appropriate hypothesis, we prove that the sequent calculus modulo is an instance of the powerful framework of abstract canonical systems and that therefore, cuts correspond to critical proofs that abstract completion allows us to eliminate. In addition to an original and deep understanding of the interactions between deduction and computation and of the expressivity of abstract canonical systems, this provides a mechanical way to transform a sequent calculus modulo into an equivalent one admitting the cut rule, therefore extending in a significant way the applicability of mechanized proof search in deduction modulo

Guillaume Burel et Claude Kirchner. Completion is an instance of abstract canonical system inference. In Kokichi Futatsugi, Jean Pierre Jouannaud et José Meseguer (dir.), Algebra, Meaning and Computation, volume 4060 de LNCS, pages 497-520. Springer, 2006. .pdf  .tex  .bib  ©SpringerAbstract Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures. Since this abstract framework is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. This has been done for ground completion (where all equational axioms are ground) but was still an open question for the general completion process. By showing that the standard completion is an instance of the ACSI framework we close the question. For this purpose, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the abstract canonical system framework.

Acceptées (Workshops)

Guillaume Burel. A Shallow Embedding of Resolution and Superposition Proofs into the lamdba-Pi-Calculus Modulo, présenté au workshop PxTP'13  .pdf

Mathieu Boespflug et Guillaume Burel. CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo, présenté au workshop PxTP'12.pdf

Guillaume Burel. Consistency Implies Cut Admissibility, présenté au workshop PSATTT'11, disponible via HAL.

Guillaume Burel et Gilles Dowek. How can we prove that a proof search method is not an instance of another?  2009Présenté par Gilles Dowek au workshop LFMTP'09.  .pdf  DOI

Guillaume Burel et Claude Kirchner. An abstract completion procedure for cut elimination in deduction modulo  2006Présentation courte à LICS'06.  .pdf

Les rares sources LaTeX accessibles ici sont incomplètes (il manque les fichiers d'entête), elles sont données uniquement au cas où elles seraient plus lisibles que les autres formats.

Voir également mes publications sur HAL (pas à jour).

Présentations

Tout d'abord, une courte présentation de mon sujet de thèse pour l'école jeunes chercheurs en programmation : .pdf  .tex

Une présentation plus longue, reprenant le travail effectué pendant mon mastère, puis introduisant les idées concernant la complétion en déduction modulo : .pdf  .tex

La présentation courte donnée à LICS'06, introduisant la complétion en déduction modulo : .pdf  .tex

Les transparents de la présentation pour LFCS'07 (Élimination des coupures en dédution modulo par complétion abstraite) : .pdf  .tex

Les transparents de la présentation pour CSL'07 (Réduction de la taille des preuves en déduction modulo) : .pdf  .tex

Une présentation de l'encodage des systèmes de type purs fonctionnels en superdeduction: .pdf  .tex

Les transparents de ma soutenance de thèse « Bonnes démonstrations en déduction modulo » : .pdf

Rapports

Mon Stage de Mastère

Je l'ai effectué en mars/août 2005 dans l'équipe PROTHEO du LORIA. Il portait sur des application du cadre des systèmes canoniques abstraits à la complétion standard (plus connue sous les jolis noms de Knuth-Bendix) et à la déduction naturelle. Ce cadre, introduit par N. Dershowitz et C. Kirchner, est une approche théorique des procédures de complétion et autres procédures similaires qui fonctionnent par saturation. Il est basé sur l'utilisation d'un ordre sur les preuves, ce qui permet de traduire la notion intuitive de "bonne preuve" par celle de preuve minimale. J'ai montré que la complétion standard rentrait bien dans ce cadre, et qu'en le généralisant un peu on pouvait aussi y faire entrer la déduction naturelle.

Rapport

Mon Stage de MIM2

Je l'ai effectué en janvier/mars 2004 à la Lehrstuhl Broy du Département Informatique de l'Université Technique de Munich. Il portait sur la génération automatique de programmes à partir d'exemples. Par exemple, 1+0=1 et 2+3=5 permettent de générer l'addition, le programme le "plus simple" qui satisfait ces contraintes. Mon approche a été d'étendre l'algorithme d'unification d'ordre supérieure de G. Huet.

Résultats

Mon Stage de MIM1

Je l'ai effectué en juin/juillet 2003 dans l'équipe PROTHEO du LORIA. Il portait sur l'utilisation en logique équationnelle (celle où l'on ne considère que des égalités entre termes quantifiées universellement) de probabilités telles qu'elles ont été introduites par J. Halpern pour la logique du premier ordre.

Mon Rapport