计算机科学中的逻辑

Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover…

We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multiple LLM-based coding agents. Rather than relying on static…

We compare three satisfiability notions for propositional formulas in the language {not, and, or} over a fixed finite-dimensional Hilbert space H=F^d with F in {R, C}. The first is the standard Hilbert-lattice semantics on the subspace…

Mining specifications from execution traces presents an automated way of capturing characteristic system behaviors. However, existing approaches are largely restricted to Boolean abstractions of events, limiting their ability to express…

Codensity monads provide a universal method to generate complex monads from simple functors. Recently, a wide range of important monads in logic, denotational semantics, and probabilistic computation, such as several incarnations of the…

We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent…

Commonly used proof strategies by automated reasoners organise proof search either by ordering-based saturation or by reducing goals to subgoals. In this paper, we combine these two approaches and advocate a SAT-based method with symmetry…

Bounded self-certification in Turing machines fails because self-simulation necessarily incurs a strictly positive temporal overhead. We translate this operational constraint into a domain-theoretic framework, defining an operator that…

Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL). This challenge is particularly pronounced when relying on compact (small and medium) language models,…

We consider the problem of modifying a description logic concept in light of models represented as pointed interpretations. We call this setting model change, and distinguish three main kinds of changes: eviction, which consists of only…

We investigate preservation results for the independent fusion of one-variable first-order modal logics. We show that, without equality, Kripke completeness and decidability of the global and local consequence relation are preserved, under…

We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality…

Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the…

We introduce the semantically-defined constructive master-modality logics $\sf CK^*$ and $\sf WK^*$, extending the basic constructive modal logic $\sf CK$ and the Wijesekera-style logic $\sf WK$ obtained by impossing infallibility. Using…

We survey systematic approaches to basis-restricted fragments of propositional logic and modal logics, with an emphasis on how expressive power and computational complexity depend on the allowed operators. The propositional case is…

Relative entropy is a fundamental class of distances between probability distributions, with widespread applications in probability theory, statistics, and machine learning. In this work, we study relative entropy from a categorical…

Formal verification of designs with multiple properties has been a long-standing challenge for the verification research community. The task of coming up with an effective strategy that can efficiently cluster properties to be solved…

We propose Fluid Logic, a paradigm in which modal logical reasoning, temporal, epistemic, doxastic, deontic, is lifted from discrete Kripke structures to continuous manifolds via Neural Stochastic Differential Equations (Neural SDEs). Each…

A type assignment system for lambda-calculus enjoys the principal typing property if every typable term M has a special typing, called principal, from which all typings for M can be obtained via suitable operations. The existence of…

Terms in the lambda-calculus can be represented as planar trees decorated with symbols for abstraction and application, and having variables as leaves. In this paper, we concentrate on the branches of such trees, rather than on the trees…