- The bounded model property via step algebras and step frames
- Annals of Pure and Applied Logic
- Volume | Issue number
- 165 | 12
- Pages (from-to)
- Document type
- Interfacultary Research Institutes
- Institute for Logic, Language and Computation (ILLC)
The paper introduces semantic and algorithmic methods for establishing a variant of the analytic subformula property (called ‘the bounded proof property’, bpp) for modal propositional logics. The bpp is much weaker property than full cut-elimination, but it is nevertheless sufficient for establishing decidability results. Our methodology originated from tools and techniques developed on one side within the algebraic/coalgebraic literature dealing with free algebra constructions and on the other side from classical correspondence theory in modal logic. As such, our approach is orthogonal to recent literature based on proof-theoretic methods and, in a way, complements it.
We applied our method to simple logics such as K, T, K4, S4, etc., where establishing basic metatheoretical properties becomes a completely automatic task (the related proof obligations can be instantaneously discharged by current first-order provers). For more complicated logics, some ingenuity is still needed, however we were able to successfully apply our uniform method to the well-known cut-free system for GL, to Goré's cut-free system for S4.3, and to Ohnishi-Matsumoto's analytic system for S5.
- go to publisher's site
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.