Minimal temporal epistemic logic (Q1815428)

The dynamics of (nonmonotonic) reasoning processes is studied. The presented approach is based on two components: Epistemic logic is used as a formalization of information states. Temporal logic is used as a formalization of a dynamics of information states. A minimal entailment construction (in the style of Shoham) is used in order, to introduce nonmonotonicity into this framework. Some basic assumptions are accepted: Reasoning is conservative, this means, the agent's knowledge increases as he is reasoning. A discrete and linear time is assumed. A temporal epistemic logic (TEL) is the basis of the framework. The epistemic language with the usual S5-semantics is introduced. Pairs \((M,m)\), where \(M\) is a normal S5-model and \(m\in M\) (inuitively, \(m\) is the current world) are called epistemic states. The epistemic language is extended by introducing temporal operators. Semantics of TEL is defined by a function from natural numbers to epistemic states, called TEL-model. Truth of a formula in a TEL-model is defined as it is usual in a temporal semantics (the basic case is truth in S5, for formulae of the epistemic language). An axiomatization of TEL is proposed. Soundness, completeness, and decidability of the system are proven. The interaction between the epistemic part and the temporal part of the logic is quite limited (by the conservativity assumption). The conservativity of the reasoning is formalized as follows. The degree-of-information ordering \(\leq\) on epistemic states is defined. A TEL model \({\mathcal M}\) is called conservative if for each natural number \(s\), \({\mathcal M}(s) \leq {\mathcal M} (s+1)\). Validity and semantical consequence restricted to the class of conservative models (TELC-models), denoted by \(\models^C\), is considered. A sound, complete, and decidable axiomatization of TELC is studied. Minimal conservative models and minimal entailment are studied over TELC. As an example it is shown that minimal entailment can capture skeptical consequence in default logic. The notion of minimal entailment is shown to be decidable. Some complexity results are proven. TELC-satisfiability is NP-complete. Minimal conservative consequence is \(\Pi^P_3\)-complete. The minimal entailment is a nonmonotonic one. The class of the formulas which can be added to the premises without disturbing any of the conclusions (called the class of downward persistent formulas) is investigated. A syntactic characterization of the downward persistent formulas is presented. Checking whether a (subjective) formula is downward persistent is co-NP-complete.