计算机科学中的逻辑

Reasoning models produce long traces of intermediate decisions and tool calls, making test-time verification important for ensuring correctness. Existing approaches either verify only the final answer, which misses early errors, or rely on…

In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use…

We illustrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic, using as illustrative examples a simple voting protocol, a simple broadcast protocol (Bracha Broadcast), and a simple agreement…

Partial algebras and datatypes are discussed with the use of signatures that allow partial functions, and a three-valued short-circuit (sequential) first order logic with a Tarski semantics. The propositional part of this logic is also…

We consider a family of two-valued "fully evaluated left-sequential logics" (FELs), of which Free FEL (defined by Staudt in 2012) is most distinguishing (weakest) and immune to atomic side effects. Next is Memorising FEL, in which…

Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present sweap, a tool for synthesis of infinite-state Linear Integer Arithmetic reactive…

Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO2, the two-variable fragment of first-order logic over finite domains.…

We introduce a non-wellfounded proof system for intuitionistic logic extended with inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. We explore the…

This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^*$ specifications, based on translation to Existential Horn Clauses (EHCs). $CTL^*$ is a powerful…

Typically, a practical algorithm of hardware verification obtains a semantic result by being applied to a particular formula $F$. That is, although this algorithm uses the specifics of $F$ (sometimes inadvertently), its result holds for all…

We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems, and thus the name, are inspired by the graph minor relation and are more flexible extensions of the well-known…

This paper studies algorithmic meta theorems for property testing with \emph{constant running time} in the bounded degree model. In (Adler, Harwath 2018) it was shown that on graph classes $\mathcal C^{w}_d$ consisting of all graphs with…

We study the status of preservation theorems such as the {\L}o\'s-Tarski theorem and the homomorphism preservation theorem in the context of semiring semantics. Semiring semantics has its origins in the provenance analysis of database…

Remote Direct Memory Access (RDMA) is a technology that allows direct memory access from the memory of one computer into that of another without involving either one's operating system. This enables high-throughput, low-latency networking,…

This paper presents differential-algebraic refinement logic (dARL) with which one can deductively verify both properties and relations of differential-algebraic programs (DAPs) that extend hybrid dynamical systems with…

Previsions are positively homogeneous functionals, and are generalized forms of integration functionals. We investigate previsions -- just previsions, not sublinear or superlinear previsions as in previous work. We show that every prevision…

Landauer's embeddings enable the reversibility of computations for non-reversible programming languages, augmenting each intermediate state with enough data to reconstruct the previous state. An interesting research question is therefore to…

We extend the two-variable logic on data words with guarded regular binary predicates of the form $\widetilde{L}(x,y)$ that is true if positions $x$ and $y$ are in the same class and the factor strictly between $x$ and $y$ is in the regular…

When using interactive theorem provers based on dependent type theory to define and reason about languages involving binding constructs, we advocate the use of a well-scoped version of the locally nameless method of representing syntax.…

And-Inverter Graph (AIG)-based logic synthesis has been a cornerstone of digital design automation for several decades. While numerous optimization techniques have been developed for both technology-independent and technology-dependent…