A general proof certification framework for modal logic

DOI10.1017/S0960129518000440zbMath1430.68416arXiv1810.10257MaRDI QIDQ5236558

Marco Volpe, Tomer Libal

Publication date: 9 October 2019

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1810.10257

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Proof search and certificates for evidential transactions

Uses Software

• Coq
• Isabelle
• Automath
• ModLeanTAP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Prefixed tableaus and nested sequents
• Natural deduction, hybrid systems and modal logics
• Proof analysis in modal logic
• Deep sequent systems for modal logic
• Gentzen calculi for modal propositional logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Cut-free sequent calculi for some tense logics
• A semantic framework for proof evidence
• Tableau methods of proof for modal logics
• Focused and Synthetic Nested Sequents
• Programming with Higher-Order Logic
• Interacting with Modal Logics in the Coq Proof Assistant
• Linear Nested Sequents, 2-Sequents and Hypersequents
• The Proof Certifier Checkers
• Focused Labeled Proof Systems for Modal Logic
• Proof Search in Nested Sequent Calculi
• Logic Programming with Focusing Proofs in Linear Logic
• Free-variable tableaux for propositional modal logics