计算机科学中的逻辑

Directed topology is an area of mathematics with applications in concurrency. It extends the concept of a topological space by adding a notion of directedness, which restricts how paths can evolve through a space and enables thereby a…

The effectful forcing technique allows one to show that the denotation of a closed System T term of type $(\iota \to \iota) \to \iota$ in the set-theoretical model is a continuous function $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. For…

In this paper, we introduce a novel team semantics of LTL inspired by inquisitive logic. The main features of the resulting logic, we call InqLTL, are the intuitionistic interpretation of implication and the Boolean semantics of…

In this paper, we explore the issue of inconsistency handling in DatalogMTL, an extension of Datalog with metric temporal operators. Since facts are associated with time intervals, there are different manners to restore consistency when…

Temporal causality defines what property causes some observed temporal behavior (the effect) in a given computation, based on a counterfactual analysis of similar computations. In this paper, we study its closure properties and the…

In this article, we show that the now classical protocol complex approach to distributed task solvability of Herlihy et al. can be understood in standard categorical terms. First, protocol complexes are functors, from chromatic (semi-)…

The Functional Machine Calculus (FMC, Heijltjes 2022) extends the lambda-calculus with the computational effects of global mutable store, input/output, and probabilistic choice while maintaining confluent reduction and simply-typed strong…

We give an alternative proof for the existing result that recurrent graph neural networks working with reals have the same expressive power in restriction to monadic second-order logic MSO as the graded modal substitution calculus. The…

In many applications, SMT solvers are utilized to solve similar or identical tasks over time. Significant variations in performance due to small changes in the input are not uncommon and lead to frustration for users. This sort of stability…

Cumulative prospect theory (CPT) is the first theory for decision-making under uncertainty that combines full theoretical soundness and empirically realistic features [P.P. Wakker - Prospect theory: For risk and ambiguity, Page 2]. While…

In this paper we give an overview of results on the analysis of parametric linear hybrid automata, and of systems of similar linear hybrid automata: We present possibilities of describing systems with a parametric (i.e. not explicitly…

$\omega$-regular languages are a natural extension of the regular languages to the setting of infinite words. Likewise, they are recognised by a host of automata models, one of the most important being Alternating Parity Automata (APAs), a…

We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory…

The logic IK is the intuitionistic variant of modal logic introduced by Fischer Servi, Plotkin and Stirling, and studied by Simpson. This logic is considered a fundamental intuitionstic modal system as it corresponds, modulo the standard…

We are exploring the problem of building an automated reasoning procedure that adaptively tunes the high-level solving strategy for a given problem. There are two main distinctive characteristics of our approach: tuning is performed solely…

This paper introduces a novel formal SAT-based explanation model for deep learning in video understanding. The proposed method integrates SAT solving techniques with the principles of formal explainable AI to address the limitations of…

Traditional category theory is typically based on set-theoretic principles and ideas, which are often non-constructive. An alternative approach to formalizing category theory is to use E-category theory, where hom sets become setoids. Our…

We introduce First-Order Coalition Logic ($\mathsf{FOCL}$), which combines key intuitions behind Coalition Logic ($\mathsf{CL}$) and Strategy Logic ($\mathsf{SL}$). Specifically, $\mathsf{FOCL}$ allows for arbitrary quantification over…

Distributed knowledge is one of the better known group knowledge modalities. While its intuitive idea is relatively clear, there is ample room for interpretation of details. We investigate 12 definitions of distributed knowledge that differ…

In order to get $\lambda$-models with a rich structure of $\infty$-groupoid, which we call "homotopy $\lambda$-models", a general technique is described for solving domain equations on any cartesian closed $\infty$-category (c.c.i.) with…