计算机科学中的逻辑

We study strictly positive logics in the language $\mathscr{L}^+$, which constructs formulas from $\top$, propositional variables, conjunction, and diamond modalities. We begin with the base system $\bf K^+$, the strictly positive fragment…

In this work, we present two results: The first result is the formalization of Tutte's theorem in Lean, a key theorem concerning matchings in graph theory. As this formalization is ready to be integrated in Lean's mathlib, it provides a…

In this paper, we give several equivalent characterizations for a category with finite biproducts and the sum operation of arrows, and called categories satisfying these semiadditive $\mathbf{C}\mathbf{Mon}$-categories. This allow us to…

This paper introduces a generalised opinion model that extends the standard DeGroot model by representing agents' opinions and influences as soft constraints rather than single real values. This allows for modelling scenarios beyond the…

The $\pi$-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how $\pi$-calculus processes can be controlled so that computations…

Blockchain consensus protocols enable participants to agree on consistent views of the blockchain that may be ahead or behind relative to each other but do not fork into different chains. A number of recently popular…

We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing…

Micro-Stipula is a stateful calculus in which clauses can be activated either through interactions with the external environment or by the evaluation of time expressions. Despite the apparent simplicity of its syntax and operational model,…

For many standard models of random structure, first-order logic sentences exhibit a convergence phenomenon on random inputs. The most well-known example is for random graphs with constant edge probability, where the probabilities of…

We consider multiple-environment Markov decision processes (MEMDP), which consist of a finite set of MDPs over the same state space, representing different scenarios of transition structure and probability. The value of a strategy is the…

The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also…

Session types provide a typing discipline for message-passing systems. However, their theory often assumes an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in…

Markov chains and Markov decision processes (MDPs) are well-established probabilistic models. While finite Markov models are well-understood, analysing their infinite counterparts remains a significant challenge. Decisiveness has proven to…

Proof scores can be regarded as outlines of the formal verification of system properties. They have been historically used by the OBJ family of specification languages. The main advantage of proof scores is that they follow the same syntax…

Completion is a well-known transformation that captures the stable model semantics of logic programs by turning a program into a set of first-order definitions. Stable models are models of the completion, but not all models of the…

We formalise the notion of an anonymous public announcement in the tradition of public announcement logic. Such announcements can be seen as in-between a public announcement from ``the outside" (an announcement of $\phi$) and a public…

We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that can simulate (and be simulated by) Turing Machines with a…

We introduce a version of probabilistic Kleene algebra with angelic nondeterminism and a corresponding class of automata. Our approach implements semantics via distributions over multisets in order to overcome theoretical barriers arising…

We introduce partial Markov categories. In the same way that Markov categories encode stochastic processes, partial Markov categories encode stochastic processes with constraints, observations and updates. In particular, we prove a…

Higher-order unification has been shown to be undecidable. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has most general unifiers. We extend the algorithm to…