A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi

Authors: Marta Bílková
Publication year: 2011
Publication type: Konferenční příspěvek (mezinárodní konf.)
Periodical: Logic, Language, and Computation
Projects: Dynamic Formal Systems
Bibliographic citation: BÍLKOVÁ, Marta. A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi. In: BEZHANISHVILI, N., LÖBNER, S., SCHWABE, K., SPADA, L., eds. Logic, Language, and Computation. Berlin: Springer, 2011, S. 30-45. Lecture Notes in Artificial Intelligence, 6618. ISBN 978-3-642-22302-0. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-642-22303-7_3
DOI: 10.1007/978-3-642-22303-7_3
ID: 358360

Abstract

This paper answers one rather particular question: how to perform a proof of uniform interpolation property in deep inference calculi for modal logics. We show how to perform a proof of uniform interpolation property in deep inference calculus for the basic modal logic K via forgetting a variable in a certain normal form constructed by backward proof search. For that purpose we modify the framework of deepinference calculus using a cover modality on the meta level to structure deep sequents.