WestminsterResearch

Invariant-free deduction for CTL*: the tableau method

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