@inproceedings{5cd974cac0484f91af48fa89174a4ef7,
title = "Machine-checked interpolation theorems for substructural logics using display calculi",
abstract = "We present a mechanised formalisation, in Isabelle/HOL, of Brotherston and Gor{\'e}{\textquoteright}s proof of Craig interpolation for a large of class display calculi for various propositional substructural logics. Along the way, we discuss the particular difficulties associated with the local interpolation property for various rules, and some important differences between our proofs and those of Brotherston and Gor{\'e}, which are motivated by the ease of mechanising the development. Finally, we discuss the value for this work of using a prover with a programmable user interface (here, Isabelle with its Standard ML interface).",
keywords = "Craig interpolation, Display logic, Interactive theorem proving",
author = "Dawson, {Jeremy E.} and James Brotherston and Rajeev Gor{\'e}",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 8th International Joint Conference on Automated Reasoning, IJCAR 2016 ; Conference date: 27-06-2016 Through 02-07-2016",
year = "2016",
doi = "10.1007/978-3-319-40229-1_31",
language = "English",
isbn = "9783319402284",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "452--468",
editor = "Nicola Olivetti and Ashish Tiwari",
booktitle = "Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings",
address = "Germany",
}