Mechanising Gödel-Löb provability logic in HOL light

DOI10.1007/s10817-023-09677-zMaRDI QIDQ6050769

Cosimo Perini Brogi, Marco Maggesi

Publication date: 19 September 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

higher-order logicprovability logicHOL light theorem provermechanised mathematics

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Completeness and decidability results for CTL in constructive type theory
• Natural deduction calculi and sequent calculi for counterfactual logics
• Does the deduction theorem fail for modal logic?
• Proof analysis in modal logic
• Deep sequent systems for modal logic
• Gentzen calculi for modal propositional logic
• Proof methods for modal and intuitionistic logics
• An elementary proof of the completeness of PDL
• Provability interpretations of modal logic
• Cut-free sequent calculi for some tense logics
• The genesis of possible worlds semantics
• Towards mechanical metamathematics
• Untersuchungen über das logische Schliessen. I
• Untersuchungen über das logische Schliessen. II
• First-order modal logic
• A benchmark method for the propositional modal logics K, KT, S4
• Proof-theoretic analysis of the logics of agency: the deliberative STIT
• Mechanised modal model theory
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• Proofs and countermodels in non-classical logics
• Decision procedures and expressiveness in the temporal logic of branching time
• A henkin-style completeness proof for the modal logic S5
• GEOMETRISATION OF FIRST-ORDER LOGIC
• Countermodels from Sequent Calculi in Multi-Modal Logics
• Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics
• Proof Analysis
• CSL-lean: A Theorem-prover for the Logic of Comparative Concept Similarity
• NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics
• A Standard Internal Calculus for Lewis’ Counterfactual Logics
• The Method of Tree-Hypersequents for Modal Propositional Logic
• Theorem proving for conditional logics: CondLean and GOALDUCK
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• Optimizing proof search in model elimination
• HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• Automated Reasoning with Analytic Tableaux and Related Methods
• Analytic Tableaux for KLM Preferential and Cumulative Logics
• KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning
• Automated Reasoning with Analytic Tableaux and Related Methods
• Calculi, countermodel generation and theorem prover for strong logics of counterfactual reasoning

This page was built for publication: Mechanising Gödel-Löb provability logic in HOL light