HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)

DOI10.1007/978-3-030-51054-1_23MaRDI QIDQ5049016zbMATH OpenOpenAlexFDO

Authors Tiziano Dalmonte, N. Olivetti, G. L. Pozzato

Publication date 9 November 2022

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-51054-1_23

zbMATH Keywords

hypersequent calculinon-normal modal logicsprolog

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Modal Logic for Coalitional Power in Games
• Combining monotone and normal modal logic in nested sequents -- with countermodels
• Countermodel construction via optimal hypersequent calculi for non-normal modal logics
• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 1414365 (Why is no real title available?)
• Knowledge means ‘all’, belief means ‘most’
• lean\(T^ AP\): Lean tableau-based deduction
• Neighborhood semantics for modal logic
• Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi
• SAT-based decision procedures for classical modal logics
• Sequent calculi and decision procedures for weak modal systems

Cited in

(2)

• Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity
• Mechanising Gödel-Löb provability logic in HOL light

Describes a project that uses

Uses Software

• leanTAP

This page was built for publication: HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)

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