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

Corresponding author: Dragan Doder ( ddoder@mas.bg.ac.rs )

© Dragan Doder, Zoran Ognjanović, Zoran Marković.
This article is freely available under the J.UCS Open Content License.
Citation: Doder D, Ognjanović Z, Marković Z (2010) An Axiomatization of a First-order Branching Time Temporal Logic. JUCS - Journal of Universal Computer Science 16(11): 1439-1451. https://doi.org/10.3217/jucs-016-11-1439
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