计算机科学中的逻辑

We study the problem of deciding whether a point escapes a closed subset of $\mathbb{R}^d$ under the iteration of a continuous map $f \colon \mathbb{R}^d \to \mathbb{R}^d$ in the bit-model of real computation. We give a sound partial…

Is there an algorithm that takes a game in normal form as input, and outputs a Nash equilibrium? If the payoffs are integers, the answer is yes, and lot of work has been done in its computational complexity. If the payoffs are permitted to…

In \cite{Craig}, we introduced a syntactically defined and highly general class of calculi known as \emph{semi-analytic}. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must…

This work explores the potential of spatial model checking of polyhedral models on a number of selected examples. In computer graphics polyhedral models can be found in the form of triangular surface meshes of tetrahedral volume meshes…

The notion of homomorphism indistinguishability offers a combinatorial framework for characterizing equivalence relations of graphs, in particular equivalences in counting logics within finite model theory. That is, for certain graph…

In these notes we propose a new, simpler proof system for first-order matching logic with application and definedness. The new proof system is inspired by Tarski's axiomatization for first order-logic with equality (simplified by Kalish and…

This invited paper presents an overview of an ongoing research program aimed at extending the Curry-Howard-Lambek correspondence to quantum computation. We explore two key frameworks that provide both logical and computational foundations…

State-of-the-art methods for rare event simulation of non-Markovian models face practical or theoretical limits if observing the event of interest requires prior knowledge or information on the timed behavior of the system. In this paper,…

Enumerating the result set of a first-order query over a relational structure of bounded degree can be done with linear preprocessing and constant delay. In this work, we extend this result towards the compressed perspective where the…

We study algorithms to analyze a particular class of Markov population processes that is often used in epidemiology. More specifically, Markov binomial chains are the model that arises from stochastic time-discretizations of classical…

Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safety-critical ones. However, DNN verifiers are themselves…

We forge connections between the theory of fractal sets obtained as attractors of iterated function systems and process calculi. To this end, we reinterpret Milner's expressions for processes as contraction operators on a complete metric…

We introduce the class of tree constraint automata with data values in Z (equipped with the less than relation and equality predicates to constants) and we show that the nonemptiness problem is ExpTime-complete. Using an automata-based…

This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next…

This paper develops a comprehensive framework for artificial intelligence systems that operate under strict epistemic constraints, moving beyond stochastic language prediction to support structured reasoning, propositional commitment, and…

This article develops a novel framework for modal logic based on the idea of stratified actualization, rather than the classical model of global possible worlds. Traditional Kripke semantics treat modal operators as quantification over…

I present a model of universal parallel computation called $\Delta$-Nets, and a method to translate $\lambda$-terms into $\Delta$-nets and back. Together, the model and the method constitute an algorithm for optimal parallel…

This paper studies the expected value of multiplicative rewards, where rewards obtained in each step are multiplied (instead of the usual addition), in Markov chains (MCs) and Markov decision processes (MDPs). One of the key differences to…

While there is a long tradition of reasoning about (non)termination in program analysis, specialized logics are typically needed to give different termination criteria. This includes partial correctness, where termination is not guaranteed,…

In this note we provide an algorithm for translating relational structures into "proper" relational structures, i.e., those such that there is no pair of worlds w and u such that w is accessible from u for every agent. In particular, our…