Publication Date:
2011-11-24
Description:
We give a sound and complete labelled natural deduction system for a bundled branching temporal logic, namely the until-free version of BCTL *. The logic BCTL * is obtained by referring to a more general semantics than that of CTL *, where we only require that the set of paths in a model is closed under taking suffixes (i.e. is suffix-closed) and is closed under putting together a finite prefix of one path with the suffix of any other path beginning at the same state where the prefix ends (i.e. is fusion-closed). In other words, this logic does not enjoy the so-called limit-closure property of the standard CTL * validity semantics. We give both a classical and an intuitionistic version of our labelled natural deduction system for the until-free version of BCTL *, and carry out a proof-theoretical analysis of the intuitionistic system: we prove that derivations reduce to a normal form, which allows us to give a purely syntactical proof of consistency (for both the intuitionistic and classical versions) of the deduction system.
Print ISSN:
0955-792X
Electronic ISSN:
1465-363X
Topics:
Computer Science
,
Mathematics
Permalink
