Cut-free sequent systems for temporal logic (Q941433)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 5318672
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Cut-free sequent systems for temporal logic |
scientific article; zbMATH DE number 5318672 |
Statements
Cut-free sequent systems for temporal logic (English)
0 references
1 September 2008
0 references
The paper develops finitary cut-free, invariant-free, weakening-free, and contraction-free sequent calculi for the propositional temporal logics LTL and CTL, using the earlier developed idea of focus games [see, e.g., \textit{M. Lange} and \textit{C. Stirling}, J. Log. Comput. 12, No.~4, 623--639 (2002; Zbl 1001.68077)]. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics.
0 references
temporal logic
0 references
LTL
0 references
CTL
0 references
cut-free sequent calculus
0 references
focus games
0 references
0 references
0.8397984504699707
0 references
0.8252725005149841
0 references
0.8230763673782349
0 references
0.8122340440750122
0 references
