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

Publications

Submitted/unpublished manuscripts

Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory, PDF

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

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

Accepted (Journals and Conferences)

Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand and Olivier Hermant. First-order automated reasoning with theories: When deduction modulo theory meets practice. Journal of Automated Reasoning, 64(6):1001-1050, 2020. .pdf  .bib  ©Springer.Abstract We discuss the practical results obtained by the first generation of automated theorem provers based on Deduction Modulo Theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with the introduction of a rewrite feature. Deduction Modulo Theory is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We introduce two automated reasoning systems that have been built to extend other provers with Deduction Modulo Theory. The first one is Zenon Modulo, a tableau-based tool able to deal with polymorphic first-order logic with equality, while the second one is iProverModulo, a resolution-based system dealing with first-order logic with equality. We also provide some experimental results run on benchmarks that show the beneficial impact of the extension on these two tools and their underlying proof search methods. Finally, we describe the two backends of these systems to the Dedukti universal proof checker, which also relies on Deduction Modulo Theory, and which allows us to verify the proofs produced by these tools.

Guillaume Burel. Linking focusing and resolution with selection. ACM Transactions on Computational Logic, 21:18:1-30, 2020. .pdf  .bib  ACM DL.Abstract Focusing and selection are techniques that shrink the proof-search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atomic formula can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof-search space.

Catherine Dubois, Virgile Prevosto and Guillaume Burel. Teaching formal methods to future engineers. In Luigia Petre, Brijesh Dongol and Graeme Smith (eds.), FMTEA 2019, volume 11758 of LNCS, pages 69-80. Springer, 2019. ©Springer.Abstract Formal methods provide systematic and rigorous techniques for software development. We are convinced that they must be taught in Software Engineering curricula. In this paper, we present a set of formal methods courses included in a Software Engineering & Security track of ENSIIE, École Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise, a French engineering school delivering the ``Ingénieur de l'ENSIIE'' degree (master level). These techniques have been taught over the last fifteen years in our education programs in different formats. One of the difficulty we encounter is that students consider these kinds of techniques difficult and requiring much work and thus are inclined to choose other courses when they can. Furthermore, students are strongly focused on the direct applicability of the knowledge they are taught, and they are not all going to pursue a professional career in the development of critical systems. Our experience shows that students can gain confidence in formal methods when they understand that, through a rigorous mathematical approach to system specification, they acquire knowledge, skills and abilities that will be useful in their professional future as Computer Scientists/Engineers.

Guillaume Burel. Linking focusing and resolution with selection. In Igor Potapov, Paul Spirakis and James Worrell (eds.), MFCS 2018, volume 117 of LIPIcs, pages 9:1-9:14. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2018. .pdf  .bib  DROPS. See also the journal version with full proofs.Abstract Focusing and selection are techniques that shrink the proof search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atom can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof search space.

Guillaume Burel, Gilles Dowek and Ying Jiang. A completion method to decide reachability in rewrite systems. In Carsten Lutz and Silvio Ranise (eds.), Frontiers of Combining Systems, volume 9322 of LNCS, pages 205-219. Springer, 2015. .bib  ©Springer.Abstract The Knuth-Bendix method takes in argument a finite set of equations and rewrite rules and, when it succeeds, returns an algorithm to decide if a term is equivalent to another modulo these equations and rules. In this paper, we design a similar method that takes in argument a finite set of rewrite rules and, when it succeeds, returns an algorithm to decide not equivalence but reachability modulo these rules, that is if a term reduces to another. As an application, we give new proofs of the decidability of reachability in finite ground rewrite systems and in pushdown systems.

Guillaume Burel. Cut admissibility by saturation. In Gilles Dowek (ed.), RTA-TLCA, volume 8560 of LNCS, pages 124-138. Springer, 2014. .pdf  .bib  ©Springer.Abstract Deduction modulo is a framework in which theories are integrated into proof systems such as natural deduction or sequent calculus by presenting them using rewriting rules. When only terms are rewritten, cut admissibility in those systems is equivalent to the confluence of the rewriting system, as shown by Dowek, RTA 2003, LNCS 2706. This is no longer true when considering rewriting rules involving propositions. In this paper, we show that, in the same way that it is possible to recover confluence using Knuth-Bendix completion, one can regain cut admissibility in the general case using standard saturation techniques. This work relies on a view of proposition rewriting rules as oriented clauses, like term rewriting rules can be seen as oriented equations. This also leads us to introduce an extension of deduction modulo with conditional term rewriting rules.

Guillaume Burel and Simon Cruanes. Detection of first-order axiomatic theories. In Pascal Fontaine, Christophe Ringeissen and Renate Schmidt (eds.), FroCoS, volume 8152 of 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 and Nikolaj Bj{\o}rner (eds.), CADE, volume 6803 of 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 and Helmut Veith (eds.), CSL, volume 6247 of 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 and 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 and Roberto Sebastiani (eds.), FroCoS, volume 5749 of 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. Ph.D. thesis, Université Henri Poincaré (Nancy 1), 2009. .pdf .bib TELAbstract This thesis studies how computations may simplify proofs and aims to make mechanized proof search better. We are particularly interested in deduction modulo and superdeduction, two close formalisms allowing the integration of computations into proofs through a rewrite system. We consider three simplicity criteria related to proof search.
Cut admissibility makes it possible to restrain the proof-search space but does not always hold in deduction modulo. We define a completion method transforming a rewrite system representing computations so that at the end cut admissibility holds. By the way, we show how to transform any first-order theory to integrate it into the computational part of proofs.
We show then how deduction modulo unboundedly reduces proof lengths, by transferring deduction steps into computations. In particular, we apply this to higher-order arithmetic to show that proof-length speedups between ith- and i+1st-order arithmetic disappear when working in deduction modulo, making it possible to work in first-order logic modulo without increasing proof lengths.
Following this last result, we investigate which higher-order systems can be simulated in first order using deduction modulo. We are interested by pure type systems, which are generic type systems for the lambda-calculus with dependent types. We show how these systems can be encoded in superdeduction. This offers new perspectives on their normalization and on proof search within them. We also develop a methodology to describe how superdeduction can be used to specify deductive systems.

Guillaume Burel. A first-order representation of pure type systems using superdeduction. In Frank Pfenning (ed.), 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 and Thomas Henziger (eds.), CSL, volume 4646 of 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 and Claude Kirchner. Cut elimination in deduction modulo by abstract completion. In Sergei N. Artemov and Anil Nerode (eds.), LFCS, volume 4514 of 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 and Claude Kirchner. Completion is an instance of abstract canonical system inference. In Kokichi Futatsugi, Jean Pierre Jouannaud and José Meseguer (eds.), Algebra, Meaning and Computation, volume 4060 of 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.

Accepted (Workshops)

Ali Assaf and Guillaume Burel. Translating HOL to Dedukti, presented at the workshop PxTP'15  EPTCS

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

Mathieu Boespflug and Guillaume Burel. CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo, presented at the PxTP'12 workshop.  .pdf

Guillaume Burel. Consistency Implies Cut Admissibility, presented at the workshop on PSATTT'11, available through HAL.

Guillaume Burel and Gilles Dowek. How can we prove that a proof search method is not an instance of another?  2009Presented by Gilles Dowek at the workshop LFMTP'09.  .pdf  DOI

Guillaume Burel and Claude Kirchner. An abstract completion procedure for cut elimination in deduction modulo  2006Short presentation given at LICS'06.  .pdf

The rare LaTeX sources here are incomplete (the included files are absent), they are given in case they are more readable than other formats.

See also my publication list on HAL (not up-to-date).

Talks

A short presentation of my thesis for the école jeunes chercheurs en programmation : .pdf  .tex

A longer presentation, with the work done during my master, and then introducing the ideas of the completion in deduction modulo : .pdf  .tex

The short presentation given at LICS'06, introducing completion in deduction modulo : .pdf  .tex

The slides for the LFCS'07 talk (Cut elimination in deduction modulo by abstract completion): .pdf  .tex

The slides for the CSL'07 talk (Unbounded proof-length speed-up in deduction modulo): .pdf  .tex

Some presentation of the encoding of functional Pure Type Systems in superdeduction: .pdf  .tex

The slides of my PhD defense « Good Proofs in Deduction Modulo »: .pdf

Reports

Master's thesis

I did it in March/August 2005 in the team PROTHEO at the LORIA. It was on the application of Abstract Canonical Systems framework to the standard completion (a.k.a. Knuth-Bendix completion) and to natural deduction. This framework, introduced by N. Dershowitz and C. Kirchner, is a theoretical approach of completion procedures and of other procedures working by saturation. It is based on the introduction of some order over the proofs. This order is used to represent the intuitive notion of "good proofs" by minimal proofs. I proved that standard completion was an instance of this framework, and that we can generalize this framework somehow to capture the natural deduction too.

Report

My stage of maîtrise

I did it in January/March 2004 at the Lehrstuhl Broy of the Department of Informatics of the Technische Universität München. It dealt with the automatic generation of programs through examples. For instance, 1+0=1 and 2+3=5 permit to generate the addition, the "simplest" program which satisfies these constraints. My approach was to extend G. Huet's higher order unification algorithm.

Results

My stage of licence

I did it in June/July 2003 in the team PROTHEO at the LORIA. It was on the use in equational logic (where one consider only universally quantified equalities between terms) of probabilities in the same way they were introduced by J. Halpern for first order logic.

Report