International Conference on Formal and Applied
Practical Reasoning (FAPR'96),
Bonn, Germany,
June 37,
1996.
LNCS 1085, Springer,
pp. 399413.
A Tableau Calculus For FirstOrder Branching Time Logic
Wolfgang May, Peter H. Schmitt
Abstract:
Tableaubased proof systems have been designed for many logics extending
classical firstorder logic.
This paper proposes a sound tableau calculus for temporal logics of the
firstorder CTLfamily.
Until now, a tableau calculus has only been presented for the
propositional version of CTL.
The calculus considered operates with prefixed formulas and may be
regarded as an instance of a labelled deductive system.
The prefixes allow an explicit partial description of states and paths
of a potential Kripke counter model in the tableau.
It is possible in particular to represent path segments of finite but
arbitrary length which are needed to process reachability formulas.
Furthermore, we show that by using prefixed formulas and explicit
representation of paths it becomes possible to express and process
fairness properties without having to resort to full CTL^{*}.
The approach is suitable for use in interactive proofsystems.
[PSFile]
[Slides]


