计算机科学中的逻辑

We propose a calculus of string diagrams to reason about satisfiability of Boolean formulas, and prove it to be sound and complete. We then showcase our calculus in a few case studies. First, we consider SAT-solving. Second, we consider…

In 2009, Ghani, Hancock and Pattinson gave a tree-like representation of stream processors $A^{\mathbb{N}} \rightarrow B^{\mathbb{N}}$. In 2021, Garner showed that this representation can be established in terms of algebraic theory and…

We argue that operads provide a general framework for dealing with polynomials and combinatory completeness of combinatory algebras, including the classical $\mathbf{SK}$-algebras, linear $\mathbf{BCI}$-algebras, planar…

In this paper, we give an overview of some recent work on applying tools from category theory in finite model theory, descriptive complexity, constraint satisfaction, and combinatorics. The motivations for this work come from Computer…

Traditionally, Epistemic Logic represents epistemic scenarios using a single model. This, however, covers only complete descriptions that specify truth values of all assertions. Indeed, many -- and perhaps most -- epistemic descriptions are…

Distributive laws are a standard way of combining two monads, providing a compositional approach for reasoning about computational effects in semantics. Situations where no such law exists can sometimes be handled by weakening the notion of…

The problem of identifying a probabilistic context free grammar has two aspects: the first is determining the grammar's topology (the rules of the grammar) and the second is estimating probabilistic weights for each rule. Given the hardness…

The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings.…

The `mathematical language' Automath, conceived by N.G. de Bruijn in 1968, was the first theorem prover actually working and was used for checking many specimina of mathematical content. Its goals and syntactic ideas inspired Th. Coquand…

Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties…

In order to apply canonical labelling of graphs and isomorphism checking in interactive theorem provers, these checking algorithms must either be mechanically verified or their results must be verifiable by independent checkers. We analyze…

We describe a model for polarization in multi-agent systems based on Esteban and Ray's standard family of polarization measures from economics. Agents evolve by updating their beliefs (opinions) based on an underlying influence graph, as in…

Uniform coloured Petri nets can be abstracted to their skeleton, the place/transition net that simply turns the coloured tokens into black tokens. A coloured net and its skeleton are related by a net morphism. For the application of the…

Partial synchrony is a model of computation in many distributed algorithms and modern blockchains. These algorithms are typically parameterized in the number of participants, and their correctness requires the existence of bounds on message…

We present two deductively equivalent calculi for non-deterministic many-valued logics. One is defined by axioms and the other - by rules of inference. The two calculi are obtained from the truth tables of the logic under consideration in a…

Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for…

Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for…

An order-theoretic forest is a countable partial order such that the set of elements larger than any element is linearly ordered. It is an order-theoretic tree if any two elements have an upper-bound. The order type of a branch can be any…

We tackle the problem of establishing the soundness of approximate bisimilarity with respect to PCTL and its relaxed semantics. To this purpose, we consider a notion of bisimilarity inspired by the one introduced by Desharnais, Laviolette,…

We present a call-by-need $\lambda$-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit…