计算机科学中的逻辑

We show that the category OS of operator spaces, with complete contractions as morphisms, is locally countably presentable and a model of Intuitionistic Linear Logic in the sense of Lafont. We then describe a model of Classical Linear…

In France, the first year of study at university is usually abbreviated L1 (for premiere annee de Licence). At Sorbonne Paris Nord University, we have been teaching an 18 hour introductory course in formal proofs to L1 students for 3 years.…

MiniCalc is a web app for teaching first-order logic based on a minimal sequent calculus. As an option the proofs can be verified in the Isabelle proof assistant. We present the lessons learned using the tool in recent years at our…

OnlineProver is an interactive proof assistant tailored for the educational setting. Its main features include a user-friendly interface for editing and checking proofs. The user interface provides feedback directly within the derivation,…

We report on recent improvements to the free logic education software tool GNU Aris, including the latest features added during the Google Summer of Code 2023 project. We focused on making GNU Aris a web application to enable almost all…

MITL is a temporal logic that facilitates the verification of real-time systems by expressing the critical timing constraints placed on these systems. MITL specifications can be checked against system models expressed as networks of timed…

Formal verification has become increasingly important because of the kinds of guarantees that it can provide for software systems. Verification of models of biological and medical systems is a promising application of formal verification.…

The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education while favoring software support for this transition by exploiting the…

The poset cover problem seeks a minimum set of partial orders whose linear extensions cover a given set of linear orders. Recognizing its NP-completeness, we devised a non-trivial reduction to the Boolean satisfiability problem using a…

We present crest, a tool for automatically proving (non-)confluence and termination of logically constrained rewrite systems. We compare crest to other tools for logically constrained rewriting. Extensive experiments demonstrate the promise…

We study the relationship between partial map classifiers, Sierpi\'nski cones, and axioms for synthetic higher categories and domains within univalent foundations. In particular, we show that synthetic $\infty$-categories are closed under…

A number of model-comparison games central to (finite) model theory, such as pebble and Ehrenfeucht-Fra\"{i}ss\'{e} games, can be captured as comonads on categories of relational structures. In particular, the coalgebras for these comonads…

Courcelle's Theorem states that on graphs $G$ of tree-width at most $k$ with a given tree-decomposition of size $t(G)$, graph properties $\mathcal{P}$ definable in Monadic Second Order Logic can be checked in linear time in the size of…

Behind a set of rules in Deontic Defeasible Logic, there is a mapping process of normative background fragments. This process goes from text to rules and implicitly encompasses an explanation of the coded fragments. In this paper we deliver…

We tackle the problem of enumerating set-theoretic solutions to the Yang-Baxter equation. This equation originates from statistical and quantum mechanics, but also has applications in knot theory, cryptography, quantum computation and group…

We investigate the expressive power of regular expressions for languages of countable words and establish their expressive equivalence with logical and algebraic characterizations. Our goal is to extend the classical theory of regular…

Differential logical relations are a method to measure distances between higher-order programs. They differ from standard methods based on program metrics in that differences between functional programs are themselves functions, relating…

Equality saturation, a technique for program optimisation and reasoning, has gained attention due to the resurgence of equality graphs (e-graphs). E-graphs represent equivalence classes of terms under rewrite rules, enabling simultaneous…

In pioneering work from 2019, Barcel\'o and coauthors identified logics that precisely match the expressive power of constant iteration-depth graph neural networks (GNNs) relative to properties definable in first-order logic. In this…

A crucial skill for primary school teachers is maintaining efficient classroom management. Teachers use classroom seating arrangements to help maintain this efficiency. However, developing classroom seating arrangements is both…