Craig interpolation in displayable logics

James Brotherston; Rajeev Goré

doi:10.1007/978-3-642-22119-4_9

Craig interpolation in displayable logics

James Brotherston^*, Rajeev Goré

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

7 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings
Pages	88-103
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-22119-4_9
Publication status	Published - 2011
Externally published	Yes
Event	20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011 - Bern, Switzerland Duration: 4 Jul 2011 → 8 Jul 2011

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6793 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011
Country/Territory	Switzerland
City	Bern
Period	4/07/11 → 8/07/11

Access to Document

10.1007/978-3-642-22119-4_9

Cite this

Brotherston, J., & Goré, R. (2011). Craig interpolation in displayable logics. In Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings (pp. 88-103). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6793 LNAI). https://doi.org/10.1007/978-3-642-22119-4_9

@inproceedings{1d882c77857446a1ac976696b84ab433,

title = "Craig interpolation in displayable logics",

abstract = "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.",

author = "James Brotherston and Rajeev Gor{\'e}",

year = "2011",

doi = "10.1007/978-3-642-22119-4\_9",

language = "English",

isbn = "9783642221187",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "88--103",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings",

note = "20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011 ; Conference date: 04-07-2011 Through 08-07-2011",

}

Brotherston, J & Goré, R 2011, Craig interpolation in displayable logics. in Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6793 LNAI, pp. 88-103, 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, Bern, Switzerland, 4/07/11. https://doi.org/10.1007/978-3-642-22119-4_9

Craig interpolation in displayable logics. / Brotherston, James; Goré, Rajeev.
Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. 2011. p. 88-103 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6793 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

TY - GEN

T1 - Craig interpolation in displayable logics

AU - Brotherston, James

AU - Goré, Rajeev

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=79959747669&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22119-4_9

DO - 10.1007/978-3-642-22119-4_9

M3 - Conference Paper

SN - 9783642221187

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 88

EP - 103

BT - Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings

T2 - 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011

Y2 - 4 July 2011 through 8 July 2011

ER -

Brotherston J, Goré R. Craig interpolation in displayable logics. In Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. 2011. p. 88-103. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-22119-4_9

Craig interpolation in displayable logics

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this