计算机科学中的逻辑

In this paper, we generalize epistemic logic so that it can help reason about ways of combining common knowledge and distributed knowledge such as "common distributed knowledge", "distributed common knowledge", "distributed common…

Model checking with the standard Kripke models used in (Dynamic) Epistemic Logic leads to scalability issues. Hence alternative representations have been developed, in particular symbolic structures based on Binary Decision Diagrams (BDDs)…

We introduce a new logic of graded distributed belief that allows us to express the fact that a group of agents distributively believe that a certain fact holds with at least strength k. We interpret our logic by means of computationally…

In recent years, epistemic logics have been extended with operators K_ax for knowledge of (the value of) a variable x (by an agent a). We study dynamic versions of these logics, enriched with modalities for semi-public data-exchange events…

Methods for probability updating, of which Bayesian conditionalization is the most well-known and widely used, are modeling tools that aim to represent the process of modifying an initial epistemic state, typically represented by a prior…

Distributed knowledge is a key concept in the standard epistemic logic of knowledge-that. In this paper, we propose a corresponding notion of distributed knowledge-how and study its logic. Our framework generalizes two existing traditions…

Intentions are crucial for our practical reasoning. The rational intention obeys some simple logical principles, such as agglomeration and consistency, among others, motivating the search for a proper logic of intention. However, such a…

Standard epistemic logics introduce a modal operator K to represent knowledge, but in doing so they presuppose the logical apparatus they aim to explain. By contrast, this paper explores how logic may be derived from the structure of…

Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for sequential programs but much more serious issues arise with…

We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal…

Bisimulation is a concept that captures behavioural equivalence of states in a variety of types of transition systems. It has been widely studied in discrete-time settings where a key notion is the bisimulation metric which quantifies "how…

We introduce Bifurcation Logic, BL, which combines a basic classical modality with separating conjunction * together with its naturally associated multiplicative implication, that is defined using the modal ordering. Specifically, a formula…

We revisit a recent puzzle about common knowledge, the ``sailboat" case (Lederman, 2018), and argue that Lewisian common knowledge allows us to reconcile the pre-theoretical intuition that certain facts are ``public" in such situations,…

Contemporary proof assistants impose restrictive syntactic guardedness conditions that reject many valid corecursive definitions. Existing approaches to overcome these restrictions present a fundamental trade-off between coverage and…

Computational paths treat propositional equality as explicit paths built from labelled deduction steps and rewrite rules. This view originates in work by de Queiroz and collaborators [1] and yields a weak groupoid structure for equality,…

Data refinement is the standard extension of a refinement relation from programs to datatypes (i.e. a behavioural subtyping relation). Forward/backward simulations provide a tractable method for establishing data refinement, and have been…

Strategies synthesized using formal methods can be complex and often require infinite memory, which does not correspond to the expected behavior when trying to model Multi-Agent Systems (MAS). To capture such behaviors, natural strategies…

Modern machine learning pipelines are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems. Therefore, we contribute a framework for verified numerical…

The TARK conference (Theoretical Aspects of Rationality and Knowledge) is a conference that aims to bring together researchers from a wide variety of fields, including computer science, artificial intelligence, game theory, decision theory,…

It was recently shown by Atserias, Buss and Mueller that the standard complexity-theoretic conjecture NEXP not in P / poly is consistent with the relatively strong bounded arithmetic theory V^0_2, which can prove a substantial part of…