{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:24:19Z","timestamp":1763641459230},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642221187"},{"type":"electronic","value":"9783642221194"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22119-4_9","type":"book-chapter","created":{"date-parts":[[2011,6,15]],"date-time":"2011-06-15T14:21:08Z","timestamp":1308147668000},"page":"88-103","source":"Crossref","is-referenced-by-count":6,"title":["Craig Interpolation in Displayable Logics"],"prefix":"10.1007","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"N.D. Belnap Jr.","year":"1982","unstructured":"Belnap Jr., N.D.: Display logic. Journal of Philosophical Logic\u00a011, 375\u2013417 (1982)","journal-title":"Journal of Philosophical Logic"},{"key":"9_CR2","series-title":"ENTCS","first-page":"197","volume-title":"Proceedings of MFPS-26","author":"J. Brotherston","year":"2010","unstructured":"Brotherston, J.: A unified display proof theory for bunched logic. In: Proceedings of MFPS-26. ENTCS, pp. 197\u2013211. Elsevier, Amsterdam (2010)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gor\u00e9, R.: Craig interpolation in displayable logics. Tech. Rep. DTR11-1, Imperial College London (2011)","DOI":"10.1007\/978-3-642-22119-4_9"},{"key":"9_CR4","series-title":"ch. I","volume-title":"Handbook of Proof Theory","author":"S.R. Buss","year":"1998","unstructured":"Buss, S.R.: Introduction to Proof Theory. In: Handbook of Proof Theory, ch. I. Elsevier Science, Amsterdam (1998)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-14295-6_16","volume-title":"Computer Aided Verification","author":"N. Caniart","year":"2010","unstructured":"Caniart, N.: merit: An interpolating model-checker. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 162\u2013166. Springer, Heidelberg (2010)"},{"issue":"3","key":"9_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic\u00a022(3), 269\u2013285 (1957)","journal-title":"Journal of Symbolic Logic"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-45685-6_10","volume-title":"Theorem Proving in Higher Order Logics","author":"J.E. Dawson","year":"2002","unstructured":"Dawson, J.E., Gor\u00e9, R.: Formalised cut admissibility for display logic. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 131\u2013147. Springer, Heidelberg (2002)"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s11229-008-9354-2","volume":"164","author":"S. Feferman","year":"2008","unstructured":"Feferman, S.: Harmonious logic: Craig\u2019s interpolation theorem and its descendants. Synthese\u00a0164, 341\u2013357 (2008)","journal-title":"Synthese"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s11225-006-8305-5","volume":"83","author":"N. Galatos","year":"2006","unstructured":"Galatos, N., Ono, H.: Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL. Studia Logica\u00a083, 279\u2013308 (2006)","journal-title":"Studia Logica"},{"issue":"5","key":"9_CR10","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1093\/jigpal\/6.5.669","volume":"6","author":"R. Gor\u00e9","year":"1998","unstructured":"Gor\u00e9, R.: Gaggles, Gentzen and Galois: How to display your favourite substructural logic. Logic Journal of the IGPL\u00a06(5), 669\u2013694 (1998)","journal-title":"Logic Journal of the IGPL"},{"issue":"3","key":"9_CR11","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1093\/jigpal\/6.3.451","volume":"6","author":"R. Gor\u00e9","year":"1998","unstructured":"Gor\u00e9, R.: Substructural logics on display. Logic J of the IGPL\u00a06(3), 451\u2013504 (1998)","journal-title":"Logic J of the IGPL"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/978-3-540-71209-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., Majumdar, R., Xu, R.-G.: State of the union: Type inference via craig interpolation. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 553\u2013567. Springer, Heidelberg (2007)"},{"key":"9_CR13","volume-title":"12th Knowledge Representation and Reasoning Conf.","author":"B. Konev","year":"2010","unstructured":"Konev, B., Lutz, C., Ponomaryov, D., Wolter, F.: Decomposing description logic ontologies. In: 12th Knowledge Representation and Reasoning Conf. AAAI, Menlo Park (2010)"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-94-017-2798-3_7","volume-title":"Proof Theory of Modal Logic","author":"M. Kracht","year":"1996","unstructured":"Kracht, M.: Power and weakness of the modal display calculus. In: Wansing, H. (ed.) Proof Theory of Modal Logic, pp. 93\u2013121. Kluwer Academic Publishers, Boston (1996)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1023\/A:1017998605966","volume":"27","author":"G. Restall","year":"1998","unstructured":"Restall, G.: Displaying and deciding substructural logics 1: Logics with contraposition. Journal of Philosophical Logic\u00a027, 179\u2013216 (1998)","journal-title":"Journal of Philosophical Logic"},{"issue":"2","key":"9_CR18","doi-asserted-by":"publisher","first-page":"419","DOI":"10.2307\/2275398","volume":"59","author":"D. Roorda","year":"1994","unstructured":"Roorda, D.: Interpolation in fragments of classical linear logic. Journal of Symbolic Logic\u00a059(2), 419\u2013444 (1994)","journal-title":"Journal of Symbolic Logic"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/BF01349560","volume":"22","author":"A. Urquhart","year":"1993","unstructured":"Urquhart, A.: Failure of interpolation in relevant logics. Journal of Philosophical Logic\u00a022, 449\u2013479 (1993)","journal-title":"Journal of Philosophical Logic"},{"key":"9_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1280-4","volume-title":"Displaying Modal Logics","author":"H. Wansing","year":"1998","unstructured":"Wansing, H.: Displaying Modal Logics. Kluwer, Boston (1998)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22119-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,20]],"date-time":"2020-06-20T04:55:55Z","timestamp":1592628955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22119-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221187","9783642221194"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22119-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}