计算机科学中的逻辑

The quantum programming language Quipper supports circuit operations such as reversing and controlling certain quantum circuits. Additionally, Quipper provides a function called with-computed, which can be used to program circuits of the…

Definite descriptions are first-order expressions that denote unique objects. In this paper, we propose a second-order counterpart, designed to refer to unique relations between objects. We investigate this notion within the framework of…

MultiParty Session Types (MPST) provide a useful framework for safe concurrent systems. Mixed choice (enabling a participant to play at the same time the roles of sender and receiver) increases the expressive power of MPST as well as the…

Reversible concurrent calculi are abstract models for concurrent systems in which any action can potentially be undone. Over the last few decades, different formalisms have been developed and their mathematical properties have been…

We identify fragments of the arithmetic $S_1$ that enjoy nice closure properties and have exact characterization of their definable multifunctions. To do this, in the language of $S_1$, $L_1$, starting from the formula classes,…

Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e.g., OBDDs, SDDs) are…

In [Mulmuley, 1987], Mulmuley gave an algorithm reducing the computation of the matrix rank function to that of determinants, of which the proof for the verification is elementary. In this article, we formalize this argument in the bounded…

We introduce monoidal streams. Monoidal streams are a generalization of causal stream functions, which can be defined in cartesian monoidal categories, to arbitrary symmetric monoidal categories. In the same way that streams provide…

Rule-based languages lie at the core of several areas of central importance to databases and artificial intelligence such as deductive databases and knowledge representation and reasoning. Disjunctive existential rules (a.k.a. disjunctive…

The queen domination problem asks for the minimum number of queens needed to attack all squares on an $n\times n$ chessboard. Once this optimal number is known, determining the number of distinct solutions up to isomorphism has also…

Neural networks excel at pattern recognition but struggle with reliable logical reasoning, often violating basic logical principles during inference. We address this limitation by developing a categorical framework that systematically…

We define a (preorder-enriched) category $\mathsf{Met}$ of quantale-valued metric spaces and uniformly continuous maps, with the essential requirement that the quantales are continuous. For each object $(X,d,Q)$ in this category, where $X$…

This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at the semantic level and guarantees to find a counterexample…

Program synthesis is the task of automatically constructing a program conforming to a given specification. In this paper we focus on synthesis of single-invocation recursion-free functions conforming to a specification given as a logical…

This article presents a relatively complete proof calculus for the dynamic logic of communicating hybrid programs dLCHP. Beyond hybrid systems, communicating hybrid programs not only feature mixed discrete and continuous dynamics but also…

The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. The boundary between fragments for which WFOMC can be computed in polynomial time…

Krebs et al. (2007) gave a characterization of the complexity class TC0 as the class of languages recognized by a certain class of typed monoids. The notion of typed monoid was introduced to extend methods of algebraic automata theory to…

We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string…

For fragments L of first-order logic (FO) with counting quantifiers, we consider the definability problem, which asks whether a given L-formula can be equivalently expressed by a formula in some fragment of L without counting, and the more…

This paper is about the computability of the modal definability problem in classes of frames determined by Euclidean modal logics. We characterize those Euclidean modal logics such that the classes of frames they determine give rise to an…