(2012). DEL-sequents for regression and epistemic planning. Journal of Applied Non-Classical Logics: Vol. 22, No. 4, pp. 337-367. doi: 10.1080/11663081.2012.736703.

Representing an epistemic situation involving several agents obviously depends on the modeling point of view one takes. We start by identifying the types of modeling points of view which are logically possible. We call the one traditionally followed by epistemic logic the perfect external approach, because there the modeler is assumed to be an omniscient and external observer of the epistemic situation. In the rest of the paper we focus on what we call the internal approach, where the modeler is (...) one of the agents involved in the situation. For this approach we propose and axiomatize a logical formalism based on epistemic logic. This leads us to formalize some intuitions about the internal approach and about its connections with the external ones. Finally, we show that our internal logic is decidable and PSPACE-complete. (shrink)

Dynamic Epistemic Logic (DEL) deals with the representation and the study in a multi-agent setting of knowledge and belief change. It can express in a uniform way epistemic statements about: 1. what is true about an initial situation 2. what is true about an event occurring in this situation 3. what is true about the resulting situation after the event has occurred. We axiomatize within the DEL framework what we can infer about (iii) given (i) and (ii). Given three formulas (...) φ,φ' and φ" describing respectively (i), (ii) and (iii), we also show how to build a formula φ ? φ' which captures all the information which can be inferred about (iii) from φ and φ'. We show how our results extend to other modal logics than K. In our proofs and definitions, we resort to a large extent to the normal form formulas for modal logic originally introduced by Kit Fine. In a companion paper (Aucher, 2012), we axiomatize what we can infer about (ii) given (i) and (iii), and what we can infer about (i) given (ii) and (iii), and show how to build two formulas φ ? φ" and φ' ? φ" which capture respectively all the information which can be inferred about (ii) from φ and φ", and all the information which can be inferred about (i) from φ' and φ". (shrink)

After observing that the truth conditions of connectives of non–classical logics are generally defined in terms of formulas of first–order logic, we introduce ‘protologics’, a class of logics whose connectives are defined by arbitrary first–order formulas. Then, we introduce atomic and molecular logics, which are two subclasses of protologics that generalize our gaggle logics and which behave particularly well from a theoretical point of view. We also study and introduce a notion of equi-expressivity between two logics based on different classes (...) of models. We prove that, according to that notion, every pure predicate logic with \ variables and constants is as expressive as a predicate atomic logic, some sort of atomic logic. Then, we prove that the class of protologics is equally expressive as the class of molecular logics. That formally supports our claim that atomic and molecular logics are somehow ‘universal’. Finally, we identify a subclass of molecular logics that we call predicate molecular logics and which constitutes its representative core: every molecular logic is as expressive as a predicate molecular logic. (shrink)

In update logic as studied by Baltag, Moss, Solecki and van Benthem, little attention is paid to the interpretation of an action by an agent, which is just assumed to depend on the situation. This is actually a complex issue that nevertheless complies to some logical dynamics. In this paper, we tackle this topic. We also deal with actions that change propositional facts of the situation. In parallel, we propose a formalism to accurately represent an agent's epistemic state based on (...) hyperreal numbers. In that respect, we use infinitesimals to express what would surprise the agents (and by how much) by contradicting their beliefs. We also use a subjective probability to model the notion of belief. It turns out that our probabilistic update mechanism satisfies the AGM postulates of belief revision. (shrink)

In epistemic logic, some axioms dealing with the notion of knowledge are rather convoluted and difficult to interpret intuitively, even though some of them, such as the axioms.2 and.3, are considered to be key axioms by some epistemic logicians. We show that they can be characterized in terms of understandable interaction axioms relating knowledge and belief or knowledge and conditional belief. In order to show it, we first sketch a theory dealing with the characterization of axioms in terms of interaction (...) axioms in modal logic. We then apply the main results and methods of this theory to obtain specific results related to epistemic and doxastic logics. (shrink)

Knowledge based privacy policies are more declarative than traditional action based ones, because they specify only what is permitted or forbidden to know, and leave the derivation of the permitted actions to a security monitor. This inference problem is already non trivial with a static privacy policy, and becomes challenging when privacy policies can change over time. We therefore introduce a dynamic modal logic that permits not only to reason about permitted and forbidden knowledge to derive the permitted actions, but (...) also to represent explicitly the declarative privacy policies together with their dynamics. The logic can be used to check both regulatory and behavioral compliance, respectively by checking that the permissions and obligations set up by the security monitor of an organization are not in conflict with the privacy policies, and by checking that these obligations are indeed enforced. (shrink)

Knowledge based privacy policies are more declarative than traditional action based ones, because they specify only what is permitted or forbidden to know, and leave the derivation of the permitted actions to a security monitor. This inference problem is already non trivial with a static privacy policy, and becomes challenging when privacy policies can change over time. We therefore introduce a dynamic modal logic that permits not only to reason about permitted and forbidden knowledge to derive the permitted actions, but (...) also to represent explicitly the declarative privacy policies together with their dynamics. The logic can be used to check both regulatory and behavioral compliance, respectively by checking that the permissions and obligations set up by the security monitor of an organization are not in conflict with the privacy policies, and by checking that these obligations are indeed enforced. (shrink)