Certification of prefixed tableau proofs for modal logic

zbMATH Open1478.03021arXiv1609.04100MaRDI QIDQ5015283FDOQ5015283

Authors: Tomer Libal, Marco Volpe 

Publication date: 7 December 2021

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

Recommendations

• A general proof certification framework for modal logic
• TABLEAUX: A general theorem prover for modal logics
• First-order modal tableaux
• scientific article; zbMATH DE number 1765692
• On two approaches to modal theorem proving

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

• Handbook of modal logic
• A Machine-Oriented Logic Based on the Resolution Principle
• Programming with higher-order logic.
• Proof analysis in modal logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Prefixed tableaus and nested sequents
• Logic Programming with Focusing Proofs in Linear Logic
• Tableau methods of proof for modal logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• A benchmark method for the propositional modal logics K, KT, S4
• Complexity of resolution proofs and function introduction
• Free-variable tableaux for propositional modal logics
• Title not available (Why is that?)
• The Proof Certifier Checkers
• Focused labeled proof systems for modal logic

Cited In (2)

• Prefixed tableaus for three-valued modal propositional logics
• A general proof certification framework for modal logic

Uses Software

• ModLeanTAP

This page was built for publication: Certification of prefixed tableau proofs for modal logic

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