A Cyclic Proof System for Full Computation Tree Logic
Guillermo Menéndez Turata, University of Amsterdam
Full Computation Tree Logic, commonly denoted CTL*, extends Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, path quantifiers may be freely combined with temporal operators, 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 trees with back-edges. A simple annotation mechanism on formulas provides a syntactic success condition on non-axiomatic leaves to guarantee soundness. Completeness is established by relating cyclic proofs to a natural ill-founded sequent calculus for the logic. This is joint work with B. Afshari and Graham E. Leigh.