JUCS - Journal of Universal Computer Science 16(11): 1439-1451, doi: 10.3217/jucs-016-11-1439
An Axiomatization of a First-order Branching Time Temporal Logic
expand article infoDragan Doder, Zoran Ognjanović§, Zoran Marković§
‡ Belgrade University, Belgrade, Serbia§ Serbian Academy of Sciences and Arts, Belgrade, Serbia
Open Access
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