计算机科学中的逻辑

State-of-the-art neural network verifiers operate by encoding neural network verification as constraint satisfaction problems. When dealing with standard piecewise-linear activation functions, such as ReLUs, verifiers typically employ…

We study the confluence property of abstract rewriting systems internal to cubical categories. We introduce cubical contractions, a higher-dimensional generalisation of reductions to normal forms, and employ them to construct cubical…

Recent research has applied modal substitution calculus (MSC) and its variants to characterize various computational frameworks such as graph neural networks (GNNs) and distributed computing systems. For example, it has been shown that the…

Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\infty,1)$-category theory. While notoriously technical,…

In this paper, we consider event structures and their probabilistic and quantum extensions as originally defined by Winskel. If these structures have already been part of sophisticated computational models, they have rarely been directly…

We develop a generic computational model that can be used effectively for establishing the existence of winning strategies for concrete finite combinatorial games. Our modelling is (equational) logic-based involving advanced techniques from…

We study Two-Variable First-Order Logic, FO2, under semantic constraints that model hierarchically structured data. Our first logic extends FO2 with a linear order < and a chain of increasingly coarser equivalence relations E_1, E_2, ... .…

We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond…

This paper synthesizes a series of formal proofs to construct a unified theory on the logical limits of the Symbol Grounding Problem. We distinguish between internal meaning (sense), which formal systems can possess via axioms, and external…

We introduce the first order logic of proofs $FOLP^\Box$ in the joint language combining justification terms and binding modalities. The main issue is Kripke--style semantics for this logic. We describe models for $FOLP^\Box$ in terms of…

Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate…

G\"odel's Dialectica interpretation is a fundamental tool for the extraction of computational content from proofs, and plays a central role in today's proof mining program. In the past decades, it has also been studied from the perspective…

Labelled tableaux have been a traditional approach to define satisfiability checking procedures for Modal Logics. In many cases, they can also be used to obtain tight complexity bounds and lead to efficient implementations of reasoning…

Sorting algorithms are fundamental to computer science, and their correctness criteria are well understood as rearranging elements of a list according to a specified total order on the underlying set of elements. As mathematical functions,…

We present a proof system that extends action logic by omega iteration, which is viewed as infinitary multiplicative conjunction. We prove cut admissibility and establish complexity bounds for the provability predicate.

We devise two complementary characterizations of hereditary history-preserving bisimilarity (HHPB): a denotational one, based on stable configuration structures, and an operational one, formulated in a reversible process calculus. Our…

We present a compositional framework for certifying resource bounds in typed programs. Terms are typed with synthesized bounds drawn from an abstract resource lattice, enabling uniform treatment of time, memory, gas, and domain-specific…

Bounded model checking (BMC) is a widely used technique for formal property verification (FPV), where the transition relation is repeatedly unrolled to increasing depths and encoded into Boolean satisfiability (SAT) queries. As the bound…

Combinational equivalence checking (CEC) remains a challenge EDA task in the formal verification of datapath circuits due to their complex arithmetic structures and the limited capability or scalability of SAT, BDD, and exact-simulation…

Definite descriptions are expressions of the form "the unique $x$ satisfying property $C$," which allow reference to objects through their distinguishing characteristics. They play a crucial role in ontology and query languages, offering an…