Publications
Manuscrits soumis/non publiés
Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory, PDF
.From Axioms to Rewriting Rules. .pdf Tableau des résultats détaillés par domaines.
.Normalization in Supernatural deduction and in Deduction modulo , 2010. .pdf
.Acceptées (Journaux et conférences)
. 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 et Graeme Smith (dir.), FMTEA 2019, volume 11758 de 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 et James Worrell (dir.), MFCS 2018, volume 117 de 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 et Silvio Ranise (dir.), Frontiers of Combining Systems, volume 9322 de 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 (dir.), RTA-TLCA, volume 8560 de 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 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.
. Experimenting with deduction modulo. In Viorica Sofronie-Stokkermans et Nikolaj Bj{\o}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.
. 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 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.
.
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 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.
.
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.
. 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.
. 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.
. 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
. 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)
Translating HOL to Dedukti, présenté au workshop PxTP'15. EPTCS
.A Shallow Embedding of Resolution and Superposition Proofs into the lamdba-Pi-Calculus Modulo, présenté au workshop PxTP'13. .pdf
.CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo, présenté au workshop PxTP'12. .pdf
.Consistency Implies Cut Admissibility, présenté au workshop PSATTT'11, disponible via HAL.
.How can we prove that a proof search method is not an instance of another? 2009. Présenté par Gilles Dowek au workshop LFMTP'09. .pdf DOI
.An abstract completion procedure for cut elimination in deduction modulo 2006. Pré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
- Le programme permettant de
générer des programmes à partir d'exemples. Après décompression, un
simple
make
devrait suffir. (Désolé, pas de tutoriel.) - Le rapport en .ps
- Ainsi que les sources. (Nécessite le programme pour les annexes.)
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.