计算机科学中的逻辑

This paper explores epistemic realizability, a form of realizability in which the property that a piece of data constitutes evidence for a logical proposition is semi-decidable. In this framework, each proposition A is assigned a verifier}…

In this paper, we present a hypersequent calculus for bimodal logic GR, where the two modalities represent the arithmetic provability predicates of Goedel and Rosser, respectively. We prove the cut-elimination theorem for the calculus.

Non-wellfounded proof systems impose a global condition called the global trace condition (GTC) on a derivation tree to ensure soundness. Providing a categorical characterisation of the GTC that guarantees soundness remains challenging due…

Over the past several decades, CDCL SAT solvers have proven remarkably effective on large industrial formulas, despite SAT being NP-complete and widely believed to be intractable. While considerable empirical research has been done on…

We establish a connection between two results in the literature on probabilistic semantics: a formulation of De Finetti's theorem in the language of category theory due to Jacobs and Staton, and the generic construction of the free…

We present Kofola, an efficient tool for complementation and inclusion checking of B\"uchi automata, two central tasks in automata-theoretic verification with applications in model checking, monitoring, and theorem proving. Kofola…

Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in…

Synthesising autonomous agents that can navigate uncertain environments while adhering to complex temporal constraints remains a fundamental challenge. While Linear Temporal Logic (LTL) provides a rigorous language for specifying such…

Dynamic Epistemic Logic extends classical epistemic logic by modeling not only static knowledge but also its evolution through information updates. Among its various systems, Public Announcement Logic (PAL) provides one of the simplest and…

Effective usage of approximate circuits for various performance trade-offs requires accurate computation of error. MCAC is a novel model counting framework for exact computation of several average and worst-case error metrics that are used…

We propose a semantic foundation for logics for reasoning in settings that possess a distinction between equality of variables, a coarser equivalence of variables, and a notion of conditional independence between variables. We show that…

Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows…

This paper develops a formal logic for guises based on the work of H\'ector-Neri Casta\~neda, who understood relations from an internalist viewpoint, following Leibniz. We introduce a syntax, model theory, and proof theory for an…

This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness in the form of…

Linear-constraint loops are programs whose transition relation is specified by a system of linear inequalities. The termination problem asks, given a loop, whether it admits an infinite computation. Decidability of termination remains open…

Cubical type theories are designed around an abstract unit interval from which types of paths, used to represent equalities, are defined. Varying the operations available on this interval yields different type theories. A reversal is an…

The Guarded Fragment (GF) is a well-established decidable fragment of first-order logic. We study an extension of GF with nested equivalence relations, namely a family of distinguished binary predicates $E_1, E_2, \dots$ interpreted as…

Because CDCL produces proofs in the Resolution proof system, problems provably hard for Resolution are also provably hard for CDCL. Exponentially shorter proofs can sometimes be found using stronger proof systems such as…

Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need to repeatedly recheck their safety in full after every change.…

CSLib is an emerging Lean 4 library for computer-science formalization, but its premise-retrieval behavior is not well represented by broad mathematical theorem-proving benchmarks. We introduce CSLibPremiseBench, a reproducible…