Herod and Pilate: two tableau provers for basic hybrid logic

DOI10.1007/978-3-642-14203-1_22MaRDI QIDQ5747765zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(3)

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

Describes a project that uses

Uses Software

• OCaml
• Pilate
• Herod
• HTab
• Spartacus

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)