Bolotov, Alexander and 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.
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)|