Cut Elimination in Deduction Modulo by Abstract Completion

act Completion (Full Version) Guillaume Burel Claude Kirchner August 6, 2007 Deduction Modulo implements Poincar´e’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 objects are much more elaborated than for standard completion. Under appropriate hypo...

• Type: Conference
• Year: 2007
• Where: LFCS
• Authors: Guillaume Burel, Claude Kirchner
• Keywords: Deduction Modulo, LFCS 2007, Natural Deduction Modulo, Sequent Calculus Modulo