Open AccessKripke Incompleteness of First-order Calculi with Temporal Modalities of CTL and Near Logics
Author(s) -
Kotikova Ekaterina Alexandrovna,
Rybakov Mikhail Nikolayevich
Publication year - 2015
Publication title -
logičeskie issledovaniâ
Language(s) - English
Resource type - Journals
eISSN - 2413-2713
pISSN - 2074-1472
DOI - 10.21146/2074-1472-2015-21-1-86-99
Subject(s) - kripke structure , kripke semantics , computation tree logic , linear temporal logic , temporal logic , expressive power , computer science , mathematics , intuitionistic logic , modal logic , class (philosophy) , ctl* , calculus (dental) , intermediate logic , discrete mathematics , theoretical computer science , linear logic , description logic , artificial intelligence , medicine , biochemistry , chemistry , modal , cytotoxic t cell , polymer chemistry , in vitro , dentistry
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.