计算机科学中的逻辑

We study preservation theorems for modal logics over finite structures with respect to three fundamental semantic relations: embeddings, injective homomorphisms, and homomorphisms. We focus on classes of pointed Kripke models that are…

Recent advances in large language models have demonstrated impressive capabilities in mathematical formalization. However, existing benchmarks focus on logical verification of declarative propositions, often neglecting the task of…

We develop a discipline-agnostic emergence calculus that treats theories as fixed points of idempotent operators acting on descriptions. We show that, once processes are composable but access to the underlying system is mediated by a…

Sets of equations E play an important computational role in rewriting-based systems R by defining an equivalence relation =E inducing a partition of terms into E-equivalence classes on which rewriting computations, denoted ->R/E and called…

Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are central to human collaboration, existing tooling treats the…

Proving proof-size lower bounds for $\mathbf{LK}$, the sequent calculus for classical propositional logic, remains a major open problem in proof complexity. We shed new light on this challenge by isolating the power of structural rules,…

People increasingly use digital platforms to exchange resources in accordance with some policies stating what resources users offer and what they require in return. In this paper, we propose a formal model of these environments, focussing…

Graph neural networks (GNNs) are a widely used class of machine learning models for graph-structured data, based on local aggregation over neighbors. GNNs have close connections to logic. In particular, their expressive power is linked to…

Answer Set Programming (ASP) with stable model semantics has proven highly effective for knowledge representation and reasoning. However, the minimality requirement of stable models can be restrictive for applications requiring exploration…

Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae $\varphi,\varphi'$ whether there is a modal formula $\psi$ that separates them, in the sense that $\varphi\models\psi$ and…

This paper introduces semi-competitive differential game logic dGLsc, which enables verification of safety-critical applications that involve interactions between two agents. In dGLsc, these interactions are specified as games on hybrid…

We develop dualities for complete perfect distributive quasi relation algebras and complete perfect distributive involutive FL-algebras. The duals are partially ordered frames with additional structure. These frames are analogous to the…

Building on the collaborative Equational Theories project initiated by Terence Tao fifteen months ago, and combining it with ideas coming from machine learning and finite model theory, we construct a latent space of equational theories…

We study the model checking problem of Hyper2LTL over finite structures. Hyper2LTL is a second-order hyperlogic, that extends the well-studied logic HyperLTL by adding quantification over sets of traces, to express complex hyperproperties…

Many-valued models generalise the structures from classical model theory by defining truth values for a model with an arbitrary algebra. Just as algebraic varieties provide semantics for many non-classical propositional logics, models…

Decidability or complexity issues about the consistency problem for description logics with concrete domains have already been analysed with tableaux-based or type elimination methods. Concrete domains in ontologies are essential to…

We investigate the possibility to separate the bisimulation-invariant fragment of P from that of NP, resp. PSPACE. We build on Otto's Theorem stating that the bisimulation-invariant queries in P are exactly those that are definable in the…

We investigate the expressive power of state space models (SSM), which have recently emerged as a potential alternative to transformer architectures in large language models. Building on recent work, we analyse SSM expressiveness through…

Synthesizing controllers that enforce both safety and actuator constraints is a central challenge in the design of cyber-physical systems. State-of-the-art reachability methods based on zonotopes deliver impressive scalability, yet no…

A first-order formula is called primitive positive (pp) if it only admits the use of existential quantifiers and conjunction. Pp-formulas are a central concept in (fixed-template) constraint satisfaction since CSP($\Gamma$) can be viewed as…