Cut Elimination in Deduction Modulo by Abstract Completion
Résumé
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 has been shown to be 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. Moreover, we prove that it is even undecidable. To recover this crucial property, computation rules can be added following the classical idea of completion a la Knuth and Bendix on terms. But of course in this case the ob jects are much more elaborated and it becomes essential to use an abstract framework which in our case is the abstract canonical systems one. We show how, under appropriate hypothesis, the sequent calculus modulo can be seen as an instance of abstract canonical systems and that therefore, cuts correspond to critical proofs that abstract completion allows us to eliminate. In addition to a deeper understanding of the interaction between deduction and computation and of the expressive power of abstract canonical systems, this provides a mechanical way to transform a sequent calculus modulo a given proposition rewrite system into an equivalent one having the cut elimination property, therefore extending in a significant way the applicability of mechanized proof search in deduction modulo.
Origine : Fichiers produits par l'(les) auteur(s)