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

DOI10.1007/978-3-030-51054-1_23OpenAlexW3038674914MaRDI QIDQ5049016

Nicola Olivetti, Tiziano Dalmonte, Gian Luca 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 calculiprolognon-normal modal logics

Mathematics Subject Classification ID

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

Related Items (1)

Mechanising Gödel-Löb provability logic in HOL light

Uses Software

• leanTAP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• SAT-based decision procedures for classical modal logics
• Sequent calculi and decision procedures for weak modal systems
• lean\(T^ AP\): Lean tableau-based deduction
• Countermodel construction via optimal hypersequent calculi for non-normal modal logics
• Combining monotone and normal modal logic in nested sequents -- with countermodels
• Neighborhood semantics for modal logic
• A Modal Logic for Coalitional Power in Games
• Knowledge means ‘all’, belief means ‘most’

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