2013 | OriginalPaper | Buchkapitel
Bounded Proofs and Step Frames
verfasst von : Nick Bezhanishvili, Silvio Ghilardi
Erschienen in: Automated Reasoning with Analytic Tableaux and Related Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The longstanding research line investigating free algebra constructions 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 property. 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 powerful in applications. For simple logics such as
K
,
T
,
K4
,
S4
, etc, 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 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
.