HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Regaining Cut Admissibility in Deduction Modulo using Abstract Completion

Guillaume Burel 1, * Claude Kirchner 1, 2
* Corresponding author
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

Contributor : Guillaume Burel Connect in order to contact the contributor
Submitted on : Wednesday, November 18, 2009 - 5:49:25 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Thursday, September 23, 2010 - 10:44:58 AM


Files produced by the author(s)




Guillaume Burel, Claude Kirchner. Regaining Cut Admissibility in Deduction Modulo using Abstract Completion. Information and Computation, Elsevier, 2010, 208 (2), pp.140-164. ⟨10.1016/j.ic.2009.10.005⟩. ⟨inria-00132964v2⟩



Record views


Files downloads