计算机科学中的逻辑

This article introduces Globular, an online proof assistant for the formalization and verification of proofs in higher-dimensional category theory. The tool produces graphical visualizations of higher-dimensional proofs, assists in their…

We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we establish functional representation theorems; and we show…

Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and…

In this paper, we consider the well-known modal logics $\mathbf{K}$, $\mathbf{T}$, $\mathbf{K4}$, and $\mathbf{S4}$, and we study some of their sub-propositional fragments, namely the classical Horn fragment, the Krom fragment, the…

The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.

Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory…

The algebraic intersection type unification problem is an important component in proof search related to several natural decision problems in intersection type systems. It is unknown and remains open whether the algebraic intersection type…

We study interacting components and their compatibility with respect to synchronous and asynchronous composition. The behavior of components is formalized by I/O-transition systems. Synchronous composition is based on simultaneous execution…

After substantial progress over the last 15 years, the "algebraic CSP-dichotomy conjecture" reduces to the following: every local constraint satisfaction problem (CSP) associated with a finite idempotent algebra is tractable if and only if…

Information flow is the branch of security that studies the leakage of information due to correlation between secrets and observables. Since in general such correlation cannot be avoided completely, it is important to quantify the leakage.…

Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specifications. When an implementation fails to conform to its…

The basic notions of quantum mechanics are formulated in terms of separable infinite dimensional Hilbert space $\mathcal{H}$. In terms of the Hilbert lattice $\mathcal{L}$ of closed linear subspaces of $\mathcal{H}$ the notions of state and…

We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The…

We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a typing discipline that guarantees both normalisation of expressions and progress of processes and that…

Quasi-trees generalize trees in that the unique "path" between two nodes may be infinite and have any countable order type. They are used to define the rank-width of a countable graph in such a way that it is equal to the least upper-bound…

The finite spectrum of a first-order sentence is the set of positive integers that are the sizes of its models. The class of finite spectra is known to be the same as the complexity class NE. We consider the spectra obtained by limiting…

We study the strength of axioms needed to prove various results related to automata on infinite words and B\"uchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak…

A datatype defining rewrite system (DDRS) is an algebraic (equational) specification intended to specify a datatype. When interpreting the equations from left-to-right, a DDRS defines a term rewriting system that must be ground-complete.…

The computational properties of modal and propositional dependence logics have been extensively studied over the past few years, starting from a result by Sevenster showing NEXPTIME-completeness of the satisfiability problem for modal…

An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that…