Kripke Incompleteness of First-order Calculi with Temporal Modalities of CTL and Near Logics

Main Article Content

Е. А. Котикова
М. Н. Рыбаков

Аннотация




We study an expressive power of temporal operators used in such logics of branching time as computational tree logic or alternating-time temporal logic. To do this we investigate calculi in the first-order language enriched with the temporal operators used in such logics. We show that the resulting languages are so powerful that many ‘natural’ calculi in the languages are not Kripke complete; for example, if a calculus in such language is correct with respect to the class of all serial linear Kripke frames (even just with constant domains) then it is not Kripke complete. Some near questions are discussed.




Скачивания

Данные скачивания пока не доступны.

Article Details

Как цитировать
[1]
Е. А. Котикова и М. Н. Рыбаков. Kripke Incompleteness of First-order Calculi with Temporal Modalities of CTL and Near Logics // Логические исследования / Logical Investigations. 2018. Т. 21. № 1.
.
Раздел
Неклассические логики