An Axiomatization of a First-order Branching Time Temporal Logic
Dragan Doder (Belgrade University, Serbia)
Zoran Ognjanović (Serbian Academy of Sciences and Arts, Serbia)
Zoran Marković (Serbian Academy of Sciences and Arts, Serbia)
Abstract: We introduce a first-order temporal logic for reasoning about branching time. It is well known that the set of valid formulas is not recursively enumerable and there is no finitary axiomatization. We offer a sound and strongly complete axiomatization for the considered logic.
Keywords: branching time logic, first order logic, strong completeness
Categories: F.4.1, I.2.4