Search

We compare different epistemic notions in the presence of awareness of propositional variables: the logic of implicit knowledge (in which explicit knowledge is definable), the logic of explicit knowledge, and the logic of speculative knowledge. Speculative knowledge is a novel epistemic notion that permits reasoning about unawareness. These logics are interpreted on epistemic awareness models: these are multi-agent Kripke structures for propositional awareness (in each state an agent may only be aware of formulas containing occurrences of a subset of all propositional variables). Different notions of bisimulation are suitable for these logics. We provide correspondence between bisimulation and modal equivalence on image-finite models for these logics. Expressivity and axiomatizations are investigated for models without restrictions, and for models with equivalence relations for all agents (modeling knowledge) and awareness introspection (agents know what they are aware of). We show that the logic of speculative knowledge is as expressive as the logic of explicit knowledge, and the logic of implicit knowledge is more expressive than the two other logics. We also present expressivity results for more restricted languages. We then provide and compare axiomatizations for the three logics; the axiomatizations for speculative knowledge are novel. We compare our results to those for awareness achieved in artificial intelligence, computer science, philosophy, and economics. [ABSTRACT FROM AUTHOR]

We examine various logics that combine knowledge, awareness, and change of awareness. An agent can become aware of propositional propositions but also of other agents or of herself. The dual operation to becoming aware, forgetting, can also be modelled. Our proposals are based on a novel notion of structural similarity that we call awareness bisimulation, the obvious notion of modal similarity for structures encoding knowledge and awareness. [ABSTRACT FROM AUTHOR]

Abstract: One way of comparing knowledge representation formalisms that has attracted attention recently is in terms of representational succinctness, i.e., we can ask whether one of the formalisms allows for a more ‘economical’ encoding of information than the other. Proving that one logic is more succinct than another becomes harder when the underlying semantics is stronger. We propose to use Formula Size Games (as put forward by Adler and Immerman (2003) [1], but we present them as games for one player, called Spoiler), games that are played on two sets of models, and that directly link the length of a play in which Spoiler wins the game with the size of a formula, i.e., a formula that is true in the first set of models but false in all models of the second set. Using formula size games, we prove the following succinctness results for m-dimensional modal logic, where one has a set of indices for m modalities: (1) on general Kripke models (and also on binary trees), a definition (with ) makes the resulting logic exponentially more succinct for ; (2) several modal logics use such abbreviations , e.g., in description logics the construct corresponds to adding role disjunctions, and an epistemic interpretation of it is ‘everybody in Γ knows’. Indeed, we show that on epistemic models (i.e., -models), the logic with becomes more succinct for ; (3) the results for the logic with ‘everybody knows’ also hold for a logic with ‘somebody knows’, and (4) on epistemic models, Public Announcement Logic is exponentially more succinct than epistemic logic, if . The latter settles an open problem raised by Lutz (2006) [18]. [Copyright &y& Elsevier]

In this paper we present refinement modal logic . A refinement is like a bisimulation, except that from the three relational requirements only ‘atoms’ and ‘back’ need to be satisfied. Our logic contains a new operator ∀ in addition to the standard box modalities for each agent. The operator ∀ acts as a quantifier over the set of all refinements of a given model. As a variation on a bisimulation quantifier, this refinement operator or refinement quantifier ∀ can be seen as quantifying over a variable not occurring in the formula bound by it. The logic combines the simplicity of multi-agent modal logic with some powers of monadic second-order quantification. We present a sound and complete axiomatization of multi-agent refinement modal logic. We also present an extension of the logic to the modal μ -calculus, and an axiomatization for the single-agent version of this logic. Examples and applications are also discussed: to software verification and design (the set of agents can also be seen as a set of actions), and to dynamic epistemic logic. We further give detailed results on the complexity of satisfiability, and on succinctness. [ABSTRACT FROM AUTHOR]