International Conference on Formal and Applied
Practical Reasoning (FAPR'96),
LNCS 1085, Springer,
A Tableau Calculus For First-Order Branching Time Logic
Wolfgang May, Peter H. Schmitt
Tableau-based proof systems have been designed for many logics extending
classical first-order logic.
This paper proposes a sound tableau calculus for temporal logics of the
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 proof-systems.