Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
A Cut-Free and Invariant-Free Sequent Calculus for PLTL
verfasst von : Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro, Fernando Orejas
Erschienen in: Computer Science Logic
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
Sequent calculi usually provide a general deductive setting that uniformly embeds other proof-theoretical approaches, such as tableaux methods, resolution techniques, goal-directed proofs, etc. Unfortunately, in temporal logic, existing sequent calculi make use of a kind of inference rules that prevent the effective mechanization of temporal deduction in the general setting. In particular, temporal sequent calculi either need some form of cut, or they make use of invariants, or they include infinitary rules. This is the case even for the simplest kind of temporal logic, propositional linear temporal logic (
PLTL
). In this paper, we provide a complete finitary sequent calculus for
PLTL
, called
$\mathcal{FC}$
, that not only is cut-free but also invariant-free. In particular, we introduce new rules which provide a new style of temporal deduction. We give a detailed proof of completeness.