Bolotov, Alexander and Gaintzarain, Jose and Lucio, Paqui (2010) Invariant-free deduction for CTL*: the tableau method. In: Bolotov, Alexander, (ed.) 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: http://www.csc.liv.ac.uk/~clare/ARW/year/2010/ARW-...
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|
|Research Community:||University of Westminster > Electronics and Computer Science, School of|
|Deposited On:||27 Jul 2012 12:20|
|Last Modified:||27 Jul 2012 12:20|
Repository Staff Only: item control page