计算机科学中的逻辑

We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proofs are notoriously correct-but-verbose and brittle across…

This paper proposes a neuro-symbolic framework for G-code generation that seeks to integrate the neural generative capabilities of the GLLM method (Abdelaal et al., 2025) with formal verification via a Separation Logic (SL) prover. To…

Safety verification in Computer Numerical Control (CNC) machining has traditionally relied on simulation-based methods that require repetitive tests when requirements change. This paper introduces a formal verification framework that…

Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their application to reasoning about probabilistic programs and…

We study existence and computability of finite bases for ideals of polynomials over infinitely many variables. In our setting, variables come from a countable logical structure A, and embeddings from A to A act on polynomials by renaming…

The Power grid is a critical infrastructure underpinning all aspects of modern society and its services. Maintaining its effectiveness requires continuous adaptations. In particular, addressing sustainability targets, demand patterns, and…

Treating syntactic equality as a logical connective -- governed by left- and right-introduction rules within the sequent calculus -- offers an elegant and powerful approach to term identity. This treatment of equality allows for the…

We study the satisfiability problem for a modal logic expressing knowing-how assertions, which captures an agent's ability to achieve a given goal under the standard semantics based on linear plans. Our main result shows that satisfiability…

Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables the automated construction of proven-to-be-correct programs,…

Sound event reports often compress timed boundary behavior into frame, segment, or event scores. This paper defines executable boundary contracts for finite sound event traces. The frame fragment is a bounded Boolean fragment embeddable in…

We propose a novel acceleration technique for loops operating on arrays. The goal of acceleration is to characterize the transitive closure of loops in a logic which is suitable for automated reasoning. Using the new notion of inductive…

Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most…

Interpretations are a fundamental tool in mathematical logic, allowing structures to be encoded within other structures via logical definitions. We study $\MSO$ \emph{multidimensional point interpretations}, where elements of an interpreted…

Reasoning about array data structures is a key requirement for many applications in hardware and software verification, especially in combination with machine integers. The Satisfiability Modulo Theories (SMT) theory of extensional arrays…

In A Study of Spinoza's Ethics (1984, {\S}17), Jonathan Bennett argues that the demonstration of Proposition V of Spinoza's Ethica contains identifiable invalid moves and that, even granted those moves, "cannot yield more than the…

We introduce a contravariant idempotent adjunction between (i) the category of ranked monads on $\mathsf{Set}$; and (ii) the category of internal categories and internal retrofunctors in the category of locales. The left adjoint takes a…

Recent research has established complexity results for the problem of deciding the existence of interpolants in logics lacking the Craig Interpolation Property (CIP). The proof techniques developed so far are non-constructive, and no…

We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following reductions: (i) a polynomial-time reduction from the…

We consider the complexity of the open-world query answering problem, where we wish to determine certain answers to conjunctive queries over incomplete datasets specified by an initial set of facts and a set of guarded TGDs. This problem…

In this paper, we propose the frameworks of generalized performance evaluation and generalized controller synthesis. To this end, we give a true concurrent process calculus as the model of systems, and present a lattice-valued performance…