|
 
|
[Bur14] Cut Admissibility by Saturation
Conférence Internationale avec comité de lecture : Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, July 2014, Vol. 8560, pp.124-138, Series LNCS, Vienna, Austria, (DOI: 10.1007/978-3-319-08918-8_9)Mots clés: deduction modulo sequent calculus resolution and superposition completion conditional rewriting
Résumé:
Deduction modulo is a framework in which theories are integrated into proof systems such as natural deduction or sequent calculus by presenting them using rewriting rules. When only terms are rewritten, cut admissibility in those systems is equivalent to the confluence of the rewriting system, as shown by Dowek, RTA 2003, LNCS 2706. This is no longer true when considering rewriting rules involving propositions. In this paper, we show that, in the same way that it is possible to recover confluence using Knuth-Bendix completion, one can regain cut admissibility in the general case using standard saturation techniques. This work relies on a view of proposition rewriting rules as oriented clauses, like term rewriting rules can be seen as oriented equations. This also leads us to introduce an extension of deduction modulo with /conditional/ term rewriting rules.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| Bur14, | |||
| title | = | "{Cut Admissibility by Saturation}", | |
| author | = | " G. Burel ", | |
| booktitle | = | "{Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications}", | |
| year | = | 2014, | |
| month | = | "July", | |
| series | = | "LNCS", | |
| volume | = | 8560, | |
| pages | = | "124-138", | |
| address | = | "Vienna, Austria", | |
| doi | = | "10.1007/978-3-319-08918-8_9", | |
| } | |||
