Craig interpolation in displayable logics.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
(pp. 88 - 103).
We give a general proof-theoretic method for proving Craig interpolation for displayable logics, based on an analysis of the individual proof rules of their display calculi. Using this uniform method, we prove interpolation for a spectrum of display calculi differing in their structural rules, including those for multiplicative linear logic, multiplicative additive linear logic and ordinary classical logic. Our analysis of proof rules also provides new insights into why interpolation fails, or seems likely to fail, in many substructural logics. Specifically, contraction appears particularly problematic for interpolation except in special circumstances. © 2011 Springer-Verlag.
|Title:||Craig interpolation in displayable logics|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science > Computer Science|
Archive Staff Only