Herod and Pilate: two tableau provers for basic hybrid logic

DOI10.1007/978-3-642-14203-1_22zbMATH Open1291.68333OpenAlexW1539127213MaRDI QIDQ5747765FDOQ5747765

Authors: Marta Cialdea Mayer, Serenella Cerrito 

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_22

Recommendations

• An efficient approach to nominal equalities in hybrid logic tableaux
• scientific article; zbMATH DE number 1341482
• Tableau-based Decision Procedures for Hybrid Logic
• HTab: a terminating tableaux system for hybrid logic
• Lightweight hybrid tableaux

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Cites Work

• Termination for Hybrid Tableaus
• A benchmark method for the propositional modal logics K, KT, S4
• An efficient approach to nominal equalities in hybrid logic tableaux

Cited In (3)

• A prover dealing with nominals, binders, transitivity and relation hierarchies
• Experiments in theorem proving for topological hybrid logic
• An efficient approach to nominal equalities in hybrid logic tableaux

Uses Software

• OCaml
• Herod
• Pilate
• Spartacus
• HTab

This page was built for publication: Herod and Pilate: two tableau provers for basic hybrid logic

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