Explore the vast range of titles available.

This paper introduces a natural deduction calculus for intuitionistic logic of belief IEL - which is easily turned into a modal λ -calculus giving a computational semantics for deductions in IEL - . By using that interpretation, it is also proved that IEL - has good proof-theoretic properties . The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in IEL - showing the general structure of such a modality for belief in an intuitionistic framework.

We present our library for universal algebra in the UniMath framework dealing with multi-sorted signatures, their algebras and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic.

We present a novel approach to modelling and verifying ant colony pathfinding behaviour in an idealised scenario mirroring the double bridge experiment from biological research. We implement our analysis framework in the HOL Light proof assistant to provide rigorous verification of emergent collective dynamics. Unlike most of the existing approaches, which are limited by state explosion or fixed-size constraints, we formally prove that an ant colony of any size converges on the optimal path, given specified preconditions. This establishes that the selection of a shortest path is a stable, emergent property independent of the colony’s population . To enhance the computational performance of the analysis on colonies of a given size, we implement a faithful translation between HOL Light and SMT-LIB2. This bridge allows proof obligations to be discharged efficiently by modern SAT solvers, thereby integrating the expressive power of higher-order logic with the speed of automated reasoning tools, and creating a division of labour between formal verification and dynamic simulation. Our work advances the application of computerised mathematics to collective adaptive systems, providing a unified framework for modelling, simulation, and formal verification.

We introduce our implementation in HOL Light of the metatheory for Gödel–Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we develop here to formalise the modal completeness proof overcomes the technical difficulty due to the non-compactness of GL and is an adaptation—according to the formal language and tools at hand—of the proof given in George Boolos’ 1995 monograph. Our theorem prover for GL relies then on this formalisation, is implemented as a tactic of HOL Light that mimics the proof search in the labelled sequent calculus G3KGL, and works as a decision algorithm for the provability logic: if the algorithm positively terminates, the tactic succeeds in producing a HOL Light theorem stating that the input formula is a theorem of GL; if the algorithm negatively terminates, the tactic extracts a model falsifying the input formula. We discuss our code for the formal proof of modal completeness and the design of our proof search algorithm. Furthermore, we propose some examples of the latter’s interactive and automated use.

We introduce our implementation in HOL Light of the metatheory for Gödel-Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we develop here to formalise the modal completeness proof overcomes the technical difficulty due to the non-compactness of GL and is an adaptation -- according to the formal language and tools at hand -- of the proof given in George Boolos' 1995 monograph. Our theorem prover for GL relies then on this formalisation, is implemented as a tactic of HOL Light that mimics the proof search in the labelled sequent calculus G3KGL, and works as a decision algorithm for the provability logic: if the algorithm positively terminates, the tactic succeeds in producing a HOL Light theorem stating that the input formula is a theorem of GL; if the algorithm negatively terminates, the tactic extracts a model falsifying the input formula. We discuss our code for the formal proof of modal completeness and the design of our proof search algorithm. Furthermore, we propose some examples of the latter's interactive and automated use.

We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories, and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic.

We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a proof assistant. By constituting a formal system for isolating the invariants of the theory we are interested in -- that is, general algebraic structures modulo isomorphism -- Univalent Mathematics seems to provide a suitable environment to carry on our endeavour.

Intuitionistic belief has been axiomatized by Artemov and Protopopescu as an extension of intuitionistic propositional logic by means of the distributivity scheme K, and of co-reflection \\(A A\\). This way, belief is interpreted as a result of verification, and it fits an extended Brouwer-Heyting-Kolmogorov interpretation for intuitionistic propositional logic with an epistemic modality. In the present paper, structural properties of a natural deduction system \\(IEL^-\\) for intuitionistic belief are investigated. The focus is on the analyticity of the calculus, so that the normalization theorem and the subformula property are proven firstly. From these, decidability and consistency of the logic follow as corollaries. Finally, disjunction properties, \\(\\)-primality, and admissibility of reflection rule are established by using purely proof-theoretic methods.

This paper introduces a natural deduction calculus for intuitionistic logic of belief \\(IEL^-\\) which is easily turned into a modal \\(\\)-calculus giving a computational semantics for deductions in \\(IEL^-\\). By using that interpretation, it is also proved that \\(IEL^-\\) has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in \\(IEL^-\\) showing the general structure of such a modality for belief in an intuitionistic framework.

This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices in structuring proofs which make essential use of the tools of HOL Light and which differ in part from the standard strategies found in main textbooks covering the topic in an informal setting. Moreover, we propose a reflection on our own experience in using this specific theorem prover for this formalization task, with an analysis of pros and cons of reasoning within and about the formal system for GL we implemented in our code.