1,720,978 research outputs found
Investigations of proof theory and automated reasoning for non-classical logics
Full text linkThis thesis presents some new results in structural proof theory for modal, intuitionistic, and intuitionistic modal logics.
The first part introduces three original Gentzen-style natural deduction calculi for, respectively, intuitionistic verification-based epistemic states -- namely, belief and knowledge operators -- and intuitionistic strong L\"ob logic for arithmetical provability. For each of these calculi strong normalisation results are proven w.r.t. several systems of proof rewritings, which are considered on the basis of their structural relevance, e.g.\ for establishing the related subformula principles, or for providing a categorical semantics of normal deductions. The presentation of new and original sequent calculi for a wide family of interpretability logics closes this first part of the thesis. These sequent systems are modularly designed by recurring to internalisation techniques which make possible their fine grained structural analysis, this way establishing both their semantic and structural completeness.
The second part has a more applicative nature. It presents first an implementation in the HOL Light proof assistant of an internal theorem prover and countermodel constructor for G\"odel-L\"ob logic, relying on a previous computerised proof of modal completeness for that logic within the same formal environment. The design of that proof search algorithm is surveyed, and examples of both its interactive and automated use are shown. An overview of an ongoing automation-oriented implementation in UniMath of the basics of univalent universal algebra closes this second part of the thesis. The coding style and methodology used are discussed besides some concrete formalisation examples of algebraic structures.
Finally, two appendices describe the logical engine underlying each of the proof assistants that are used for the results presented in the second part, namely classical higher order logic for HOL Light, and univalent type theory for UniMath
Growing a Modular Framework for Modal Systems: HOLMS
Full text linkWe present HOLMS (HOL Light Library for Modal Systems), an evolving modular framework for mechanising modal reasoning within the HOL Light proof assistant. Building on earlier work on Gödel-Löb logic (GL), HOLMS introduces a compositional architecture to formalise modal adequacy proofs and implement automated decision procedures for various normal modal systems, currently including K, T, K4, and GL. To clarify the compositional nature of our framework and illustrate how it bridges general-purpose proof assistants, enriched sequent calculi, and formalised mathematics, we highlight some design choices and structural features of HOLMS, such as its use of the metalanguage, embedding strategies, and modularity metrics
A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS
Full text linkWe communicate here the most recent extension of HOLMS, our library for modal logics aimed at introducing automated modal reasoning within the HOL Light proof assistant. Based on a uniform proof strategy, we present a more refined formal proof of completeness for systems within and beyond the S5-normal modal cube, notably Gödel-Löb logic. We report on our development by adopting a measure of its modularity based on Strachey’s distinction between parametric and ad hoc polymorphic code
Growing HOLMS, a HOL Light Library for Modal Systems
Full text linkThis paper introduces HOLMS (HOL-Light Library for Modal Systems), a new framework within the HOL Light proof assistant, designed for automated theorem proving and countermodel construction in modal logics. Building on our prior work focused on Gödel-Löb logic (GL), we generalise our approach to cover a broader range of normal modal systems, starting here with the minimal system K. HOLMS provides a flexible mechanism for automating proof search and countermodel generation by leveraging labelled sequent calculi, interactive theorem proving, and formal completeness results. It thus offers the inception of a comprehensive tool for modal logic reasoning at a high level of confidence and automation. Our on-going HOLMS project aims to create a uniform, scalable method for handling multiple modal systems within HOL Light, thereby advancing the automation of modal reasoning within proof assistants
- …
