计算机科学中的逻辑

Formalization of mathematics is a major topic, that includes in particular numerical analysis, towards proofs of scientific computing programs. The present study is about the finite element method, a popular method to numerically solve…

One of the advantages of LTL over CTL is that the notion of a counterexample is easy to grasp, visualise and process: it is a trace that violates the property at hand. In this paper we propose a notion of evidence for CTL properties on…

We present a search for small Kochen-Specker (KS) sets in dimension 3, specifically targeting extensions of the 13-ray Yu-Oh set, which has been proven to be the minimal witness to state-independent contextuality. To enable this search, we…

Inductive definitions are an important form of knowledge. The logic FO(ID) is an extension of classical first-order logic FO with general non-monotone inductive definitions. Most existing proof systems for inductive definitions impose…

Autonomous systems increasingly execute actions that directly modify shared state, creating an urgent need for precise control over which transitions are permitted to occur. Existing governance mechanisms evaluate policies prior to…

We introduce APPL (Abstract Program Property Logic), a unifying Hoare-style logic that subsumes standard Hoare logic, incorrectness logic, and several variants of Hyper Hoare logic. APPL provides a principled foundation for abstract program…

In the rewriting logic framework, equational-based specifications are used to define deterministic functional behavior, abstract data types, and canonical representations of data. These specifications include a (possibly order-sorted)…

Generative AI systems are known to amplify biases present in their training data. While several inference-time mitigation strategies have been proposed, they remain largely empirical and lack formal guarantees. In this paper we introduce…

We study constraint satisfaction problems (CSPs) where the constraint languages are defined by finite automata, giving rise to automata-based CSPs. The key notion is the concept of Automatic Constraint Satisfaction Problem ($AutCSP$), where…

Streamliner constraints reduce the search space of combinatorial problems by ruling out portions of the solution space. We adapt the StreamLLM approach, which uses Large Language Models (LLMs) to generate streamliners for Constraint…

In this article, the hierarchy of LFIs L$_n^k$, Logics of Controlled Consistency (LCC), is introduced. Inspired by da Costa's original C$_n$ systems, this hierarchy can represent different degrees of paraconsistent commitment and different…

Tape diagrams provide a convenient graphical notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$. In this work, we introduce Kleene-Cartesian rig categories, namely rig…

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be…

We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jancar and Purser, 2019] holds even for a simple subclass of conservative nets. As our main result, we prove that for structurally live conservative nets, the…

AuDaLa is a recently introduced programming language that follows the new data autonomous paradigm. In this paradigm, small pieces of data execute functions autonomously. Considering the paradigm and the design choices of AuDaLa, it is…

A central computational task in database theory, finite model theory, and computer science at large is the evaluation of a first-order sentence on a finite structure. In the context of this task, the \emph{width} of a sentence, defined as…

We present a logical system CFP (Concurrent Fixed Point Logic) supporting the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and…

We introduce a calculus of extensional resource terms. These are resource terms \`a la Ehrhard-Regnier, but in infinitely eta-long form. The calculus still retains a finite syntax and dynamics: in particular, we prove strong confluence and…

We present a data-driven approach to the quantitative verification of probabilistic programs and stochastic dynamical models. Our approach leverages neural networks to compute tight and sound bounds for the probability that a stochastic…

We study synthesis for obligation properties expressed in LTLfp, the extension of LTLf to infinite traces. Obligation properties are positive Boolean combinations of safety and guarantee (co-safety) properties and form the second level of…