A general proof certification framework for modal logic

DOI10.1017/S0960129518000440zbMATH Open1430.68416arXiv1810.10257MaRDI QIDQ5236558FDOQ5236558

Authors: Tomer Libal, Marco Volpe 

Publication date: 9 October 2019

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

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.

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

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

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)

Cites Work

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

Cited In (7)

• Title not available (Why is that?)
• Title not available (Why is that?)
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Proof search and certificates for evidential transactions
• Formal Reasoning Using Distributed Assertions
• A complete modal proof system for HAL: the Herbrand agent language
• Certification of prefixed tableau proofs for modal logic

Uses Software

• Coq
• Isabelle
• Automath
• ModLeanTAP

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)