Thomas Agotnes, Natasha Alechina
Traditional epistemic logic assumes that agents' knowledge is closed under logical consequence. Many attempts to solve this logical omniscience problem weaken the closure condition by assuming that agents are ignorant of certain logical rules. Duc (1997) avoids the apparent paradox of non-omniscience and non-ignorance by introducing propositions on the form "A is true after some train of thought of agent i" explicitly into the language. A logic DES4n for this language is presented as a dynamic version of S4n. DES4n describes agents who do not necessarily know any (S4n) consequence of their knowledge now, but can get to know any such consequence in the future. Duc does not, however give a semantics for DES4n. In this paper we provide a semantics, for DES4n and some weaker and related systems, and prove soundness and completeness. A key assumption is that an agent can only know a finite number of formulae at each time. The semantics is based on Kripke models, where each world syntactically assigns a finite number of formulae to each agent and the transitions model steps of reasoning.
Subjects: 3.6 Temporal Reasoning; 11. Knowledge Representation
Submitted: Mar 6, 2006