2026-08-03T06:45:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17466 2024-03-06T11:00:03Z ddc:004 open_access

A Cyclic Proof System for Full Computation Tree Logic Afshari, Bahareh Leigh, Graham E. Menéndez Turata, Guillermo Full computation tree logic Hypersequent calculus Cyclic proofs Full Computation Tree Logic, commonly denoted CTL*, is the extension of Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, the path quantifiers are not bound to specific linear modalities, resulting in a more expressive language. We present a sound and complete hypersequent calculus for CTL*. The proof system is cyclic in the sense that proofs are finite derivation trees with back-edges. A syntactic success condition on non-axiomatic leaves guarantees soundness. Completeness is established by relating cyclic proofs to a natural ill-founded sequent calculus for the logic. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bahareh Afshari and Graham E. Leigh and Guillermo Menéndez Turata 2023 Is Part Of LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2023.5 urn:nbn:de:0030-drops-174664 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.5 eng https://creativecommons.org/licenses/by/4.0/legalcode