A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities

DOI10.1007/s10817-012-9257-2zbMath1314.03018OpenAlexW1975468279MaRDI QIDQ2351166

Serenella Cerrito, Marta Cialdea Mayer

Publication date: 23 June 2015

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

Full work available at URL: https://doi.org/10.1007/s10817-012-9257-2

zbMATH Keywords

modal logicautomated reasoningtableauxhybrid logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Combined logics (03B62)

Related Items (2)

A prover dealing with nominals, binders, transitivity and relation hierarchies ⋮ Extended decision procedure for a fragment of HL with binders

Uses Software

• Sibyl

Cites Work

• Terminating tableau systems for hybrid logic with difference and converse
• Hybrid languages
• Guarded fragments with constants
• Hybrid Logics and Ontology Languages
• A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders
• On the Restraining Power of Guards
• Computer Science Logic
• Termination for Hybrid Tableaus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities