A tableau calculus for first-order branching time logic

Abstract

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 first-order CTL-family. 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 CTLz.ast. The approach is suitable for use in interactive proof-systems.