计算机科学中的逻辑

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…

The Game Description Language (GDL) is a widely used formalism for specifying the rules of general games. Writing correct GDL descriptions can be challenging, especially for non-experts. Automated theorem proving has been proposed to assist…

Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as $\forall\exists$-formulas, expressing the…

We present a novel characterization of stable mergesort functions using relational parametricity, and show that it implies the functional correctness of mergesort. As a result, one can prove the correctness of several variations of…

We consider reachability decision problems for linear dynamical systems: Given a linear map on $\mathbb{R}^d$ , together with source and target sets, determine whether there is a point in the source set whose orbit, obtained by repeatedly…

This notes explains how a standard algorithm that constructs the discrete Fourier transform has been formalised and proved correct in the Coq proof assistant using the SSReflect extension.

Satisfiability Modulo Theory (SMT) has recently emerged as a powerful tool for solving various automated reasoning problems across diverse domains. Unlike traditional satisfiability methods confined to Boolean variables, SMT can reason on…

Interference is a phenomenon on proof systems for SAT solving that is both counter-intuitive and bothersome when developing proof-logging techniques. However, all existing proof systems that can produce short proofs for all inprocessing…

In group decisions or deliberations, stakeholders are often confronted with conflicting opinions. We investigate a logic-based way of expressing such opinions and a formal general notion of a middle ground between stakeholders. Inspired by…

The TPTP World is the well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The TPTP World supports a range of classical logics, and since release v9.0.0 has…

In this paper, we investigate the verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-constrained validity (LVP) problem for verifying GNNs…

We develop a behavioural theory of reflective parallel algorithms (RAs), i.e. synchronous parallel algorithms that can modify their own behaviour. The theory comprises a set of postulates defining the class of RAs, an abstract machine…