计算机科学中的逻辑
Arboreal categories were introduced as an axiomatic framework for game comonads, which provide a comonadic view on many model-comparison games in logic. We demonstrate the inadequacy of the axiom stating that paths are connected. We then…
We propose a method for reasoning about trust in multi-agent systems, specifying a language for describing communication protocols and making trust assumptions and derivations. This is given an interpretation in a modal logic for describing…
Satisfiability solving is a common technique for formal verification forming the basis of many proof and model checking systems. Failure to show a proof obligation will produce a counterexample or failure trace with typically many thousands…
Agent frameworks increasingly encode tool-using behavior as explicit workflow graphs, yet safety enforcement remains a runtime concern. These frameworks expose analyzable graph structure through their APIs, enabling pre-deployment static…
The Busy Beaver value $S(n)$ is the maximum number of steps that an $n$-state 2-symbol Turing machine can perform from the all-zero tape before halting. $S$ was historically introduced by Tibor Rad\'o in 1962 as one of the simplest examples…
This paper introduces a new family of cognitive modal logics designed to formalize conjectural reasoning: modal systems in which cognitive contexts extend known facts with hypothetical assumptions in order to explore their consequences.…
Boolean circuits abstract away from physical details to focus on the logical structure and computational behaviour of digital components. Although such circuits have been studied for many decades, compositionality has been widely ignored or…
A Runtime Verification (RV) framework that supports online, at-speed verification of properties that can change dynamically (during in-field operations) will benefit a large variety of applications. Several state-of-the-art RV frameworks…
Chains of co-B\"uchi automata (COCOA) have recently been introduced as a new canonical model for representing arbitrary omega-regular languages. They can be minimized in polynomial time and are hence an attractive language representation…
Modern generative modelling systems are increasingly improved by expanding model capacity, training data, and computational resources. While empirical studies have documented such scaling behaviour across architectures including generative…
The decidability of a logical system refers to the existence of an algorithm that can determine whether any given formula in that system is a theorem. In this paper, Harrop's lemma is used to prove the decidability of quantum modal logic.
The expressiveness of Metric Temporal Logic (MTL) has been extensively studied throughout the last two decades. In particular, it has been shown that the \emph{interval-based} semantics of MTL is strictly more expressive than the…
Biomedical ontologies contain numerous concept or role names involving negative knowledge such as lacks_part, absence_of. Such a representation with labels rather than logical constructors would not allow a reasoner to interpret lacks_part…
Although the $\lambda$I-calculus is a natural fragment of the $\lambda$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models…
Representation theorems for formal systems often take the form of an inductive translation that satisfies certain invariants, which are proved inductively. Theory morphisms and logical relations are common patterns of such inductive…
The simulation hypothesis has recently excited renewed interest in the physics and philosophy communities. However, the hypothesis specifically concerns {\textit{computers}} that simulate physical universes. So to formally investigate the…
Kuroda's translation embeds first-order classical logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Rizkallah extended this translation to higher-order logic.…
Effectful categories have two classes of morphisms: pure morphisms, which form a monoidal category; and effectful morphisms, which can only be combined monoidally with central morphisms (such as the pure ones), forming a premonoidal…
We focus on a branch of region-based spatial logics dealing with affine geometry. The research on this topic is scarce: only a handful of papers investigate such systems, mostly in the case of the real plane. Our long-term goal is to…
We describe a new method of finding interpolants for classical logic using certain refutation system as a starting point. Refutation can be thought of as an alternative approach to the analysis of formal systems: instead of focusing on…