scientific article; zbMATH DE number 7439744

zbMath1478.03021arXiv1609.04100MaRDI QIDQ5015283

Tomer Libal, Marco Volpe

Publication date: 7 December 2021

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

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

A general proof certification framework for modal logic

Uses Software

• ModLeanTAP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Prefixed tableaus and nested sequents
• Proof analysis in modal logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Complexity of resolution proofs and function introduction
• A benchmark method for the propositional modal logics K, KT, S4
• Tableau methods of proof for modal logics
• Programming with Higher-Order Logic
• The Proof Certifier Checkers
• Focused Labeled Proof Systems for Modal Logic
• Logic Programming with Focusing Proofs in Linear Logic
• A Machine-Oriented Logic Based on the Resolution Principle
• Free-variable tableaux for propositional modal logics