Cut Admissibility by Saturation. .pdf.
Normalization in Supernatural deduction and in Deduction modulo , 2010. .pdf.
. 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ø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
Information and Computation,
.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
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.
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).
The slides of my PhD defense « Good Proofs in Deduction Modulo »: .pdf
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.
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.
- The program to
generate programs through examples. After decompression,
makeand pry. (Sorry, no tutorial available.)
- The report (.ps)
- And the sources. (Need the program sources for the appendix.)
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.