HTab: a terminating tableaux system for hybrid logic

DOI10.1016/J.ENTCS.2009.02.026MaRDI QIDQ4982111zbMATH OpenOpenAlexFDO

Authors Guillaume Hoffmann

Publication date 23 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.02.026

zbMATH Keywords

hybrid logictableaux methodtheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Combined logics (03B62) Functional programming and lambda calculus (68N18) Logic in artificial intelligence (68T27)

Recommendations

• Termination for Hybrid Tableaus
• Terminating Tableaux for Hybrid Logic with Eventualities
• Terminating tableau systems for hybrid logic with difference and converse
• Terminating Tableau Calculi for Hybrid Logics Extending K
• Terminating tableaux for graded hybrid logic with global modalities and role hierarchies

Cites work

• scientific article; zbMATH DE number 1222434 (Why is no real title available?)
• scientific article; zbMATH DE number 1765711 (Why is no real title available?)
• scientific article; zbMATH DE number 757645 (Why is no real title available?)
• scientific article; zbMATH DE number 1424043 (Why is no real title available?)
• Introduction to algorithms
• Logic for Programming, Artificial Intelligence, and Reasoning
• Termination for Hybrid Tableaus
• The price of universality

Cited in

(15)

• Terminating tableau systems for hybrid logic with difference and converse
• A goal-directed decision procedure for hybrid PDL
• HTab
• An efficient approach to nominal equalities in hybrid logic tableaux
• Hybrid specification of reactive systems: an institutional approach
• scientific article; zbMATH DE number 1950252 (Why is no real title available?)
• Terminating Tableau Calculi for Hybrid Logics Extending K
• Experiments in theorem proving for topological hybrid logic
• Relation-changing logics as fragments of hybrid logics
• Termination for Hybrid Tableaus
• Terminating Tableaux for Hybrid Logic with Eventualities
• Herod and Pilate: two tableau provers for basic hybrid logic
• \textbf{DefTab}: a tableaux system for sceptical consequence in default modal logics
• Data-aware hybrid tableaux
• Symmetric blocking

Describes a project that uses

Uses Software

• GHC
• HyLoRes
• Racer
• HyLoTab
• Haskell

This page was built for publication: HTab: a terminating tableaux system for hybrid logic

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