Publications
Submitted/unpublished manuscripts
. Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory, PDF
. From Axioms to Rewriting Rules. .pdf Table with results detailed by domains.
. Normalization in Supernatural deduction and in Deduction modulo , 2010. .pdf
Accepted (Journals and Conferences)
. 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.
. 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.
. 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.
. 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.
. 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.
. 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.
. 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.
. 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.
. 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.
. 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.
.
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.
. 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.
.
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.
. 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.
. 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.
. 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
. 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)
. Translating HOL to Dedukti, presented at the workshop PxTP'15. EPTCS
. A Shallow Embedding of Resolution and Superposition Proofs into the lamdba-Pi-Calculus Modulo, presented at the PxTP'13 workshop. .pdf
. CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo, presented at the PxTP'12 workshop. .pdf
. Consistency Implies Cut Admissibility, presented at the workshop on PSATTT'11, available through HAL.
. How can we prove that a proof search method is not an instance of another? 2009. Presented by Gilles Dowek at the workshop LFMTP'09. .pdf DOI
. An abstract completion procedure for cut elimination in deduction modulo 2006. Short 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
- The program to
generate programs through examples. After decompression,
type
makeand pry. (Sorry, no tutorial available.) - The report (.ps)
- And the sources. (Need the program sources for the appendix.)
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.
