A natural deduction system for bundled branching time logic

摘要

We introduce a natural deduction system for the until-free subsystem BCTL_-~* of the branching time logic BCTL~*. Although we work with labelled formulas, our system differs conceptually from the usual labelled deduction systems because we have no relational formulas. Moreover, no deduction rule embodies semantic features such as properties of accessibility relation or similar algebraic properties. We provide a suitable semantics for our system and prove that it is sound and weakly complete with respect to such semantics.