Cut elimination for a calculus with context-dependent rules |
| |
| Authors: | Birgit Elbl |
| |
| Affiliation: | Institut für Theoretische Informatik und Mathematik, Fakult?t für Informatik, UniBw München, 85577 Neubiberg, Germany. e-mail: birgit@informatik.unibw-muenchen.de, DE
|
| |
| Abstract: | Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers. Received: 11 April 1998 / Published online: 25 January 2001 |
| |
| Keywords: | Mathematics Subject Classification (2000): 03F05 03B60 68Q55 68N17 |
| 本文献已被 SpringerLink 等数据库收录！ |
|
