计算机科学中的逻辑

Petri nets and their variants are often considered through their interleaved semantics, i.e. considering executions where, at each step, a single transition fires. This is clearly a miss, as Petri nets are a true concurrency model. This…

We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical…

We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal mu-calculus, a question that had remained open for several decades. The proof…

Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal…

String diagrams are pictorial representations for morphisms of symmetric monoidal categories. They constitute an intuitive and expressive graphical syntax, which has found application in a very diverse range of fields including concurrency…

Substructural logics naturally support a quantitative interpretation of formulas, as they are seen as consumable resources. Distances are the quantitative counterpart of equivalence relations: they measure how much two objects are similar,…

We study multi-structural games, played on two sets $\mathcal{A}$ and $\mathcal{B}$ of structures. These games generalize Ehrenfeucht-Fra\"{i}ss\'{e} games. Whereas Ehrenfeucht-Fra\"{i}ss\'{e} games capture the quantifier rank of a…

We present a domain-theoretic framework for probabilistic programming that provides a constructive definition of conditional probability and addresses computability challenges previously identified in the literature. We introduce a novel…

We present Coalition Logic, a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm…

Behavioural conformances -- e.g. behavioural equivalences, distances, preorders -- on a wide range of system types (non-deterministic, probabilistic, weighted etc.) can be dealt with uniformly in the paradigm of universal coalgebra. One of…

We present our implementation of DRUP-based interpolants in CaDiCaL 2.0, and evaluate performance in the bit-level model checker Avy using the Hardware Model Checking Competition benchmarks. CaDiCaL is a state-of-the-art, open-source SAT…

We show that first order logic (FO) and first order logic extended with modulo counting quantifiers (FOMOD) over purely functional vocabularies which extend addition, satisfy the Crane beach property (CBP) if the logic satisfies a normal…

Modalities in homotopy type theory are used to create and access subuniverses of a given type universe. These have significant applications throughout mathematics and computer science, and in particular can be used to create universes in…

This comprehensive survey examines Lean 4, a state-of-the-art interactive theorem prover and functional programming language. We analyze its architectural design, type system, metaprogramming capabilities, and practical applications in…

In this paper, we present Real-Time Analog Monitoring Tool (RTAMT), a tool for quantitative monitoring of Signal Temporal Logic (STL) specifications. The library implements a flexible architecture that supports: (1) various environments…

Recent work by Shehper et al. (2024) demonstrated that the well-known Akbulut-Kirby AK(3) balanced presentation of the trivial group is stably AC-equivalent to the trivial presentation. This result eliminates AK(3) as a potential…

Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a surge of interest in using machine learning models in…

We present a simple functional programming language, called Dual PCF, that implements forward mode automatic differentiation using dual numbers in the framework of exact real number computation. The main new feature of this language is the…

This report defines (plain) Dag-like derivations in the purely implicational fragment of minimal logic $M_{\supset}$. Introduce the horizontal collapsing set of rules and the algorithm {\bf HC}. Explain why {\bf HC} can transform any…

In recent work, Watanabe, Eberhart, Asada, and Hasuo have shown that parity games can be seen as string diagrams, that is, as the morphisms of a symmetric monoidal category, an algebraic structure with two different operations of…