Logic of Discovery in Uncertain Situations– Deciding Algorithms

We study a logic LDU (logic of Discovery in Uncertain Situations) generated in a semantic way as the set of all formulas valid in Krike/Hintikka models, which are models of linear discrete time with time clusters imitating possible uncertain states. The possibility of discoveryand uncertain necessity of discoveryare modeled by modal operations. The logic LDU differs from all standard normal and non-normal modal logics because the modalities ate not mutually expressible in standard way. We discuss properties of this logic, i.e. study its fragments, compare LDU with well known modal logics and study the main question about decidability of this logic. We propose an algorithm recognizing theorems of LDU (so we show that LDU is decidable), which is based on verification of validity of special normal reduced forms of rules in models of quadratic polynomial size in the testing rules.