Data di Pubblicazione:
2013
Citazione:
Bounded proofs and step frames / N. Bezhanishvili, S. Ghilardi - In: Automated Reasoning with Analytic Tableaux and Related Methods / [a cura di] D. Galmiche, D. Larchey-Wendling. - [s.l] : Springer, 2013. - ISBN 978-3-642-40536-5. - pp. 44-58 (( Intervento presentato al 22. convegno TABLEAUX tenutosi a Nancy nel 2013 [10.1007/978-3-642-40537-2_6].
Abstract:
The longstanding research line investigating free algebra con-
structions in modal logic from an algebraic and coalgebraic point of view
recently lead to the notion of a one-step frame [14], [8]. A one-step frame
is a two-sorted structure which admits interpretations of modal formulae
without nested modal operators. In this paper, we exploit the potential
of one-step frames for investigating proof-theoretic aspects. This includes
developing a method which detects when a specific rule-based calculus
Ax axiomatizing a given logic L has the so-called bounded proof prop-
erty. This property is a kind of an analytic subformula property limiting
the proof search space. We define conservative one-step frames and prove
that every finite conservative one-step frame for Ax is a p-morphic image
of a finite Kripke frame for L iff Ax has the bounded proof property and
L has the finite model property. This result, combined with a ‘one-step
version’ of the classical correspondence theory, turns out to be quite pow-
erful in applications. For simple logics such as K, T, K4, S4, etc, estab-
lishing 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 ingenu-
ity is needed, however we successfully applied our uniform method to
Avron’s cut-free system for GL and to Gor ́’s cut-free system for S4.3.
Tipologia IRIS:
03 - Contributo in volume
Keywords:
modal logic ; step frames
Elenco autori:
N. Bezhanishvili, S. Ghilardi
Link alla scheda completa:
Titolo del libro:
Automated Reasoning with Analytic Tableaux and Related Methods