Lightweight hybrid tableaux

DOI10.1016/J.JAL.2010.08.003zbMATH Open1228.03004OpenAlexW2035819327MaRDI QIDQ631086FDOQ631086

Authors: Guillaume Hoffmann 

Publication date: 22 March 2011

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2010.08.003

Recommendations

• Hybrid tableaux for the difference modality
• Decision procedures for some strong hybrid logics
• Tableau-based Decision Procedures for Hybrid Logic
• Terminating tableau systems for hybrid logic with difference and converse
• Termination for Hybrid Tableaus

zbMATH Keywords

modal logicdecision procedurehybrid logictableau calculusnominalsdifference modalityconverse modalityloop-check

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Cites Work

• Introduction to algorithms
• Optimizing terminological reasoning for expressive description logics
• A description logic with transitive and inverse roles and role hierarchies
• An overview of tableau algorithms for description logics
• Terminating tableau systems for hybrid logic with difference and converse
• Hybrid tableaux for the difference modality
• Termination for Hybrid Tableaus

Cited In (6)

• Clausal graph tableaux for hybrid logic with eventualities and difference
• Clausal tableaux for hybrid PDL
• Herod and Pilate: two tableau provers for basic hybrid logic
• A goal-directed decision procedure for hybrid PDL
• Hybrid tableaux for the difference modality
• \textbf{DefTab}: a tableaux system for sceptical consequence in default modal logics

Uses Software

• KL-ONE

This page was built for publication: Lightweight hybrid tableaux

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