计算机科学中的逻辑

We use a novel type of epistemic logic, employing comparative knowledge assertions, to analyze the relative epistemic powers of individuals or groups of agents. Such comparative assertions can express that a group has the potential to…

We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor…

The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. Unlike many approaches to concurrency, we do not assume that…

Concentrated-liquidity automated market makers (CLAMMs), as exemplified by Uniswap v3, are now a common primitive in decentralized finance frameworks. Their design combines continuous trading on constant-function curves with discrete tick…

We introduce an extension of fixed-point logic ($\mathsf{FP}$) with a group-order operator ($\mathsf{ord}$), that computes the size of a group generated by a definable set of permutations. This operation is a generalization of the rank…

Coalition Logic is an important logic in logical research on strategic reasoning. In two recent papers, Li and Ju argued that generally, concurrent game models, models of Coalition Logic, have three too strong assumptions: seriality,…

The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. It can be solved in time polynomial in the domain size for sentences from the…

The approach to proof search dubbed "coinductive proof search" (CoIPS), and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized…

Functional analysis, especially the theory of Hilbert spaces and of operators on these, form an important area in mathematics. We formalized the Isabelle/HOL library Complex_Bounded_Operators containing a large amount of theorems about…

In 1928, Bernays and Schoenfinkel proved the decidability of prenex sentences whose matrices contain no function symbols, now known as the Bernays-Schoenfinkel (BS) class. We investigate the decidability of the BS class for all Goedel…

The goal of this paper is to present an ongoing formalization, in the framework provided by the Lean/Mathlib mathematical library, of the construction by Roby (1965) of the universal divided power algebra. This is an analogue, in the theory…

We address the problem of identifying a proof-theoretic framework that enables a compositional analysis of finite-trace properties in concurrent systems, with a particular focus on those specified via prefix-closure. To this end, we…

We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In…

In this note, we prove that intuitionistic modal logic LIK4 is decidable.

Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the finite element method. This article is therefore definitions,…

For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and permissions. Separation Logic is often extended to include…

We consider the problem of actively learning an unknown binary decision tree using only membership queries, a setting in which the learner must reason about a large hypothesis space while maintaining formal guarantees. Rather than…

This paper presents a formalized analysis of the sigmoid function and a fully mechanized proof of the Universal Approximation Theorem (UAT) in Isabelle/HOL, a higher-order logic theorem prover. The sigmoid function plays a fundamental role…

Modelling across engineering, systems science, and formal methods remains limited by binary relations, implicit semantics, and diagram-centred notations that obscure multilevel structure and hinder mechanisation. Hypernetwork Theory (HT)…

Traditionally, research on Craig interpolation is concerned with (a) establishing the Craig interpolation property (CIP) of a logic saying that every valid implication in the logic has a Craig interpolant and (b) designing algorithms that…