An efficient approach to nominal equalities in hybrid logic tableaux

DOI10.3166/jancl.20.39-61zbMath1242.03029MaRDI QIDQ2901189

Marta Cialdea Mayer, Serenella Cerrito

Publication date: 17 July 2012

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3166/jancl.20.39-61

zbMATH Keywords

modal logic; tableaux; hybrid logic

Mathematics Subject Classification ID

68T27: Logic in artificial intelligence

03B35: Mechanization of proofs and logical operations

03B62: Combined logics

Related Items

Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic, A prover dealing with nominals, binders, transitivity and relation hierarchies, A goal-directed decision procedure for hybrid PDL

Uses Software

• OCaml
• Sibyl
• Spartacus
• HTab
• HyLoTab

Cites Work

• Terminating tableau systems for hybrid logic with difference and converse
• A benchmark method for the propositional modal logics K, KT, S4
• A tableau decision procedure for \(\mathcal{SHOIQ}\)
• Hybrid logics: characterization, interpolation and complexity
• Resolution in Modal, Description and Hybrid Logic
• Tableau-based Decision Procedures for Hybrid Logic
• A first step towardsmodeling semistructured data in hybrid multimodal logic
• A description logic with transitive and inverse roles and role hierarchies
• A Modal Perspective on Path Constraints
• Natural Deduction for Hybrid Logic
• Internalizing labelled deduction
• Termination for Hybrid Tableaus
• Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic