Cut Elimination in Deduction Modulo by Abstract Completion

13 years 10 months ago

Download www.loria.fr

act Completion (Full Version) Guillaume Burel Claude Kirchner August 6, 2007 Deduction Modulo implements Poincar´e’s principle by identifying deduction and computation as diﬀerent 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 ﬁrst-order logic, proofs in such systems are quite diﬀerent and dramatically simpler with one cost: cut elimination may not hold anymore. We prove ﬁrst 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...

Guillaume Burel, Claude Kirchner

Real-time Traffic