Lightweight hybrid tableaux

DOI10.1016/J.JAL.2010.08.003MaRDI QIDQ631086zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(6)

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

Describes a project that uses

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)