计算机科学中的逻辑

The work described in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing,…

Approximation Fixpoint Theory (AFT) is an algebraic framework designed to study the semantics of non-monotonic logics. Despite its success, AFT is not readily applicable to higher-order definitions. To solve such an issue, we devise a…

Linear Logic refines Intuitionnistic Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which…

We show that all Sugihara monoids can be represented as algebras of binary relations, with the monoid operation given by relational composition. Moreover, the binary relations are weakening relations. The first step is to obtain an explicit…

This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory such as Agda. The difference from prior works is that these…

In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to…

A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted language with implicit names; then, a restricted calculus with…

In recent years, there has been growing interest in logics that formalise strategic reasoning about agents capable of modifying the structure of a given model. This line of research has been motivated by applications where a modelled system…

Recently, much work has been carried out to study simplicial interpretations of modal logic. While notions of (distributed) knowledge have been well investigated in this context, it has been open how to model belief in simplicial models. We…

This paper presents a formalization of the theory of amicable numbers in the Lean~4 proof assistant. Two positive integers $m$ and $n$ are called an amicable pair if the sum of proper divisors of $m$ equals $n$ and the sum of proper…

We develop the first two heap logics that have implicit heaplets and that admit FO-complete program verification. The notion of FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions are…

Rectified Linear Unit (ReLU) networks are piecewise-linear (PWL), so universal linear safety properties can be reduced to reasoning about linear constraints. Modern verifiers rely on SMT(LRA) procedures or MILP encodings, but a safety claim…

Quantifier elimination (QE) and Craig interpolation (CI) are central to various state-of-the-art automated approaches to hardware and software verification. They are rooted in the Boolean setting and are successful for, e.g., first-order…

A discrete duality is a relationship between classes of algebras and classes of relational systems (frames) resulting in two representation theorems building on the early work of J\'onsson and Tarski, Kripke, and van Benthem. In this…

Petri nets are a modeling formalism capable of describing complex distributed systems and there exists a large number of both academic and industrial tools that enable automatic verification of model properties. Typical questions include…

Convertibility checking - determining whether two lambda-terms are equal up to reductions - is a crucial component of proof assistants and dependently-typed languages. Practical implementations often use heuristics to quickly conclude that…

We consider interpolation from the viewpoint of fully automated theorem proving in first-order logic as a general core technique for mechanized knowledge processing. For Craig interpolation, our focus is on the two-stage approach, where…

The development of category theory in univalent foundations and the formalization thereof is an active field of research. Categories in that setting are often assumed to be univalent which means that identities and isomorphisms of objects…

In this work we introduce new generalised quantifiers which allow us to express the Rabin-Mostowski index of automata. Our main results study expressive power and decidability of the monadic second-order (MSO) logic extended with these…

Classical mathematical models used in the semantics of programming languages and computation rely on idealized abstractions such as infinite-precision real numbers, unbounded sets, and unrestricted computation. In contrast, concrete…