Extended decision procedure for a fragment of HL with binders

DOI10.1007/s10817-014-9307-zzbMath1314.03025OpenAlexW2021550356MaRDI QIDQ2351423

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-014-9307-z

zbMATH Keywords

modal logictableauxhybrid 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 (1)

A prover dealing with nominals, binders, transitivity and relation hierarchies

Uses Software

• Sibyl

Cites Work

• Unnamed Item
• Terminating tableau systems for hybrid logic with difference and converse
• A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities
• A tableau decision procedure for \(\mathcal{SHOIQ}\)
• A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$
• Hybrid Logics and Ontology Languages
• A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders
• A description logic with transitive and inverse roles and role hierarchies
• A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies
• Terminating Tableau Calculi for Hybrid Logics Extending K
• Computer Science Logic
• Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies

This page was built for publication: Extended decision procedure for a fragment of HL with binders