Certification of prefixed tableau proofs for modal logic

MaRDI QIDQ5015283zbMATH OpenFDO

Authors Tomer Libal, Marco Volpe

Publication date 7 December 2021

Full work available at URL https://arxiv.org/abs/1609.04100, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF2016.18

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)

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

Cites work

• A benchmark method for the propositional modal logics K, KT, S4
• A Machine-Oriented Logic Based on the Resolution Principle
• Complexity of resolution proofs and function introduction
• Focused labeled proof systems for modal logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Free-variable tableaux for propositional modal logics
• Handbook of modal logic
• scientific article; zbMATH DE number 4055570 (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?)
• Logic Programming with Focusing Proofs in Linear Logic
• Prefixed tableaus and nested sequents
• Programming with higher-order logic.
• Proof analysis in modal logic
• Tableau methods of proof for modal logics
• The Proof Certifier Checkers

Cited in

(2)

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

Describes a project that uses

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)