Invariant-free deduction for CTL*: the tableau method

Bolotov, Alexander, Gaintzarain, Jose and Lucio, Paqui (2010) Invariant-free deduction for CTL*: the tableau method. In: Proceedings of the automated reasoning workshop 2010: bridging the gap between theory and practice. ARW 2010. University of Westminster.

Full text not available from this repository.
Official URL:


We define a classical style, one-pass tableau for the full branching-time logic CTL?. This work extends previously defined tableau technique for propositional linear-time temporal logic, PLTL, giving a new decision procedure for CTL?. One of the core features of this method is that unlike any other known deduction for the full branching-time logic, it does not require any additional structures to deal with eventualities. Consequently the presented tableau method opens prospect for defining a dual sequent calculus which is cut-free and, in particular, invariant-free. We also hope that this tableau method could serve as a first-step towards an invariant-free resolution method for CTL*.

Item Type: Book Section
Subjects: University of Westminster > Science and Technology > Electronics and Computer Science, School of (No longer in use)
Depositing User: Rachel Wheelhouse
Date Deposited: 27 Jul 2012 11:20
Last Modified: 27 Jul 2012 11:20

Actions (login required)

Edit Item (Repository staff only) Edit Item (Repository staff only)