Definability in the class of all KD45-frames - computability and complexity

摘要

In the basic modal language ML(□) and in the basic modal language with the added universal modality ML(D, [U]), first-order definability of all formulas over the class of all KD45 frames is shown. Also, it is shown that the problems of modal definability of first-order sentences over the class of all KD45 frames in the languages ML(□) and ML(□, [U]) are both PSPACE-complete.