Mechanising Gödel-Löb provability logic in HOL light
From MaRDI portal
Publication:6050769
Cites work
- A benchmark method for the propositional modal logics K, KT, S4
- A henkin-style completeness proof for the modal logic S5
- A standard internal calculus for Lewis' counterfactual logics
- An elementary proof of the completeness of PDL
- Analytic Tableaux for KLM Preferential and Cumulative Logics
- Automated Reasoning with Analytic Tableaux and Related Methods
- Calculi, countermodel generation and theorem prover for strong logics of counterfactual reasoning
- CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
- Completeness and decidability results for CTL in constructive type theory
- CondLean: a theorem prover for conditional logics
- Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
- Countermodels from sequent calculi in multi-modal logics
- CSL-\textsf{lean}: a theorem-prover for the logic of comparative concept similarity
- Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
- Cut-free sequent calculi for some tense logics
- Decision procedures and expressiveness in the temporal logic of branching time
- Deep sequent systems for modal logic
- Does the deduction theorem fail for modal logic?
- First-order modal logic
- Formalized proof systems for propositional logic
- Gentzen calculi for modal propositional logic
- Geometrisation of first-order logic
- Handbook of modal logic
- scientific article; zbMATH DE number 3125693 (Why is no real title available?)
- scientific article; zbMATH DE number 3131078 (Why is no real title available?)
- scientific article; zbMATH DE number 956466 (Why is no real title available?)
- scientific article; zbMATH DE number 193320 (Why is no real title available?)
- scientific article; zbMATH DE number 732978 (Why is no real title available?)
- scientific article; zbMATH DE number 1170091 (Why is no real title available?)
- scientific article; zbMATH DE number 1489626 (Why is no real title available?)
- scientific article; zbMATH DE number 1497485 (Why is no real title available?)
- scientific article; zbMATH DE number 932649 (Why is no real title available?)
- scientific article; zbMATH DE number 5263148 (Why is no real title available?)
- scientific article; zbMATH DE number 5037198 (Why is no real title available?)
- scientific article; zbMATH DE number 3222098 (Why is no real title available?)
- scientific article; zbMATH DE number 3074068 (Why is no real title available?)
- scientific article; zbMATH DE number 7699443 (Why is no real title available?)
- HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
- KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning
- Label-free modular systems for classical and intuitionistic modal logics
- Mechanised modal model theory
- MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
- Natural deduction calculi and sequent calculi for counterfactual logics
- NESCOND: an implementation of nested sequent calculi for conditional logics
- Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi
- Optimizing proof search in model elimination
- Proof Analysis
- Proof analysis in modal logic
- Proof methods for modal and intuitionistic logics
- Proof-theoretic analysis of the logics of agency: the deliberative STIT
- Proofs and countermodels in non-classical logics
- Provability interpretations of modal logic
- Structural proof theory. With an appendix by Aarne Ranta
- The Computational Complexity of Provability in Systems of Modal Propositional Logic
- The genesis of possible worlds semantics
- The Method of Tree-Hypersequents for Modal Propositional Logic
- Theorem proving for conditional logics: CondLean and GOALDUCK
- Towards mechanical metamathematics
- Untersuchungen über das logische Schliessen. I
- Untersuchungen über das logische Schliessen. II
Cited in
(3)
This page was built for publication: Mechanising Gödel-Löb provability logic in HOL light
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6050769)
