This manuscript studies actions of communication between epistemic logic agents. It starts by looking into actions through which all/some agents share all their information, defining the model operation that transforms the model, discussing its properties, introducing a modality for describing it and providing an axiom system for the latter. The main part of the manuscript focuses on an action through which some agents share part of their information: they share all that they know about a topic defined by a given formula. Once again, the manuscript defines the model operation that transforms the model, discusses its properties, introduces a modality for describing it and provides an axiom system for the latter.
Analytic Cut in Epistemic Logics with Distributed Knowledge
Independent Researcher（独立研究者）；Graduate School of Humanities and Human Sciences Hokkaido University（北海道大学人文人文学研究科）；Faculty of Humanities and Human Sciences Hokkaido University（北海道大学人文人文学部）
Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)
Universidad Nacional de Quilmes (CONICET)（基尔梅斯国立大学（国家科学研究和技术委员会））；Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires（布宜诺斯艾利斯大学自然科学学院计算系）
Dynamic Epistemic Logic (DEL) is a logic that models information change in a multi-agent setting through the use of action models with pre- and post-conditions. In a recent work, DEL has been extended to first-order epistemic logic (DFOEL), with a proof that the resulting Epistemic Planning Problem is decidable, as long as action models pre- and post-conditions are non-modal and the first-order domain is finite. Our contribution highlights the role post-conditions have in DFOEL. We show that the Epistemic Planning Problem with possibly infinite first-order domains is undecidable if the non-mod…
In this paper, we present an alternative interpretation of propositional inquisitive logic as an epistemic logic of knowing how. In our setting, an inquisitive logic formula $α$ being supported by a state is formalized as "knowing how to resolve $α$" (more colloquially, "knowing how $α$ is true") holds on the S5 epistemic model corresponding to the state. Based on this epistemic interpretation, we use a dynamic epistemic logic with both know-how and know-that operators to capture the epistemic information behind the innocent-looking connectives in inquisitive logic. We show that the set of val…
This paper revisits the multi-agent epistemic logic presented in [10], where agents and sets of agents are replaced by abstract, intensional "names". We make three contributions. First, we study its model theory, providing adequate notions of bisimulation and frame morphisms, and use them to study the logic's expressive power and definability. Second, we show that the logic has a natural neighborhood semantics, which in turn allows to show that the axiomatization in [10] does not rely on possibly controversial introspective properties of knowledge. Finally, we extend the logic with common and …
The formal analysis of security protocols is a challenging field, with various approaches being studied nowadays. The famous Burrows-Abadi-Needham Logic was the first logical system aiming to validate security protocols. Combining ideas from previous approaches, in this paper we define a complete system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few of its properties are verifyied, using the theorem prover Lean.
DTU Compute, Technical University of Denmark（丹麦技术大学DTU计算学院）；London School of Economics（伦敦政治经济学院）；Center for Information and Bubble Studies, University of Copenhagen（哥本哈根大学信息与泡沫研究中心）
Many classical planning frameworks are built on first-order languages. The first-order expressive power is desirable for compactly representing actions via schemas, and for specifying quantified conditions such as $\neg\exists x\mathsf{blocks\_door}(x)$. In contrast, several recent epistemic planning frameworks are built on propositional epistemic logic. The epistemic language is useful to describe planning problems involving higher-order reasoning or epistemic goals such as $K_{a}\neg\mathsf{problem}$. This paper develops a first-order version of Dynamic Epistemic Logic (DEL). In this framewo…
This paper aims to give an epistemic interpretation to the tensor disjunction in dependence logic, through a rather surprising connection to the so-called weak disjunction in Medvedev's early work on intermediate logic under the Brouwer-Heyting-Kolmogorov (BHK)-interpretation. We expose this connection in the setting of inquisitive logic with tensor disjunction discussed by Ciardelli and Barbero (2019}, but from an epistemic perspective. More specifically, we translate the propositional formulae of inquisitive logic with tensor into modal formulae in a powerful epistemic language of "knowing h…
近年来，非标准认知逻辑（knowingwhether，knowinghow，knowingwhat，knowingwhy等）引起了人们越来越大的兴趣，这些逻辑中引入的新的认知模态在语义上都共享$\exists x \Box ϕ$的一般模式，例如，知道如何实现$ϕ$大致意味着存在一种方法，这样你就知道它是一种方法，以确保$ϕ$。此外，由此产生的逻辑是可判定的。受这些特定逻辑的启发，在这项工作中，我们提出了一个非常通用和强大的框架的基础上，量词自由谓词语言扩展了一个新的模态$\Box^x$，它包完全$\exists x \Box$在一起。我们表明，所得到的语言，虽然更有表现力，共享许多良好的性质的基本命题模态逻辑在任意模型，如有限树模型属性和van Bentham的特征w.r.t.一阶模态逻辑我们公理化的逻辑在S5框架与直观的公理捕捉之间的相互作用$\Box^x$和知道，运营商在认知设置。
