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-...
Abstract
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 |
| ID Code: | 10954 |
| Deposited On: | 27 Jul 2012 12:20 |
| Last Modified: | 27 Jul 2012 12:20 |
Repository Staff Only: item control page
