Regaining Cut Admissibility in Deduction Modulo using Abstract Completion

Guillaume Burel (1) , Claude Kirchner (1, 2)

1 PAREO - Formal islands: foundations and applications
2 Inria Bordeaux - Sud-Ouest

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.

Mots clés: Automated deduction; rewriting; Knuth-Bendix completion; critical proofs; cut admissibility; deduction modulo; proof ordering; abstract canonical system; computational proof

Domaines: Logique en informatique [cs.LO]

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