Related papers: Axiomatizing Category Theory in Free Logic
First-order logic (FOL) has proved to be a versatile and expressive tool as the basis of abstract modeling languages. Used to verify complex systems with unbounded domains, such as heap-manipulating programs and distributed protocols, FOL,…
Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions---that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with…
We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechanization is achieved via a shallow semantical embedding in…
Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The reason for that is that in first-order logic induction requires…
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and…
We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or…
Conditional independence has been widely used in AI, causal inference, machine learning, and statistics. We introduce categoroids, an algebraic structure for characterizing universal properties of conditional independence. Categoroids are…
We define a fragment of metric first-order temporal logic formulas that guarantees the finiteness of their table representations. We extend our fragment's definition to cover the temporal dual operators trigger and release and show that our…
Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep…
This paper proves normalisation theorems for intuitionist and classical negative free logic, without and with the $\invertediota$ operator for definite descriptions. Rules specific to free logic give rise to new kinds of maximal formulas…
We present a formalization of basics related to infinite words in the generic proof assistant Isabelle/HOL. Furthermore, we present a formalization of purely morphic and morphic languages. Finally, we present a formalized definition of…
Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type theory, by Finster, Mimram, Lucas…
Principia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory (inspired by ideas of Ernst…
We present the first verified implementation of a decision procedure for the quantifier-free theory of partial and linear orders. We formalise the procedure in Isabelle/HOL and provide a specification that is made executable using…
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a…
We provide a foundation for working with homological and homotopical methods in categorical algebra. This involves two mutually complementary components, namely (a) the strategic selection of suitable axiomatic frameworks, some well known…
Traditional category theory is typically based on set-theoretic principles and ideas, which are often non-constructive. An alternative approach to formalizing category theory is to use E-category theory, where hom sets become setoids. Our…
Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of…
Categorical models of the exponential modality of linear logic will often, but not always, support an operation of differentiation. When they do, we speak of a monoidal differential modality; when they do not, we have merely a monoidal…
The paper presents a comprehensive analysis of the European AI Act in terms of its logical modalities, with the aim of preparing its formal representation, for example, within the logic-pluralistic Knowledge Engineering Framework and…