A general proof certification framework for modal logic

DOI10.1017/S0960129518000440MaRDI QIDQ5236558zbMATH OpenFDO

Authors Tomer Libal, Marco Volpe

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

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

Abstract: One of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and produce outputs in different formats. The project ProofCert promotes the usage of a common specification language and of a small and trusted kernel in order to check proofs coming from different sources and for different logics. By relying on that idea and by using a classical focused sequent calculus as a kernel, we propose here a general framework for checking modal proofs. We present the implementation of the framework in a Prolog-like language and show how it is possible to specialize it in a simple and modular way in order to cover different proof formalisms, such as labeled systems, tableaux, sequent calculi and nested sequent calculi. We illustrate the method for the logic K by providing several examples and discuss how to further extend the approach.

Recommendations

• Certification of prefixed tableau proofs for modal logic
• The Proof Certifier Checkers
• scientific article; zbMATH DE number 6863660
• Proof analysis in modal logic
• A proposal for broad spectrum proof certificates

Cites work

• A semantic framework for proof evidence
• A systematic proof theory for several modal logics
• Certification of prefixed tableau proofs for modal logic
• Cut-free sequent calculi for some tense logics
• Deep sequent systems for modal logic
• Focused and Synthetic Nested Sequents
• Focused labeled proof systems for modal logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Free-variable tableaux for propositional modal logics
• Gentzen calculi for modal propositional logic
• scientific article; zbMATH DE number 956466 (Why is no real title available?)
• scientific article; zbMATH DE number 6863660 (Why is no real title available?)
• scientific article; zbMATH DE number 932649 (Why is no real title available?)
• scientific article; zbMATH DE number 3331288 (Why is no real title available?)
• Interacting with Modal Logics in the Coq Proof Assistant
• Labelled tree sequents, tree hypersequents and nested (deep) sequents
• Linear Nested Sequents, 2-Sequents and Hypersequents
• Logic Programming with Focusing Proofs in Linear Logic
• Natural deduction, hybrid systems and modal logics
• Prefixed tableaus and nested sequents
• Programming with higher-order logic.
• Proof analysis in modal logic
• Proof search in nested sequent calculi
• Tableau methods of proof for modal logics
• The Proof Certifier Checkers

Cited in

(7)

• A complete modal proof system for HAL: the Herbrand agent language
• Proof search and certificates for evidential transactions
• scientific article; zbMATH DE number 4037170 (Why is no real title available?)
• scientific article; zbMATH DE number 6863660 (Why is no real title available?)
• Certification of prefixed tableau proofs for modal logic
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Formal Reasoning Using Distributed Assertions

Describes a project that uses

Uses Software

• ModLeanTAP
• Coq
• Automath
• Isabelle

This page was built for publication: A general proof certification framework for modal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5236558)