Switch to: References

Add citations

You must login to add citations.
  1. An overview of tableau algorithms for description logics.Franz Baader & Ulrike Sattler - 2001 - Studia Logica 69 (1):5-40.
    Description logics are a family of knowledge representation formalisms that are descended from semantic networks and frames via the system Kl-one. During the last decade, it has been shown that the important reasoning problems (like subsumption and satisfiability) in a great variety of description logics can be decided using tableau-like algorithms. This is not very surprising since description logics have turned out to be closely related to propositional modal logics and logics of programs (such as propositional dynamic logic), for which (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Algebraic tableau reasoning for the description logic SHOQ.Jocelyne Faddoul & Volker Haarslev - 2010 - Journal of Applied Logic 8 (4):334-355.
    Download  
     
    Export citation  
     
    Bookmark  
  • ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse.Linh Anh Nguyen & Andrzej Szałas - 2011 - Studia Logica 98 (3):387-428.
    Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse ( REG c logics) and present sound and complete tableau calculi for the general satisfiability problem of REG c logics and the problem of checking consistency of an ABox w.r.t. a TBox in a REG c logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned problems, to which various (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • A tableau calculus with automaton-labelled formulae for regular grammar logics.Rajeev Gore - unknown
    We present a sound and complete tableau calculus for the class of regular grammar logics. Our tableau rules use a special feature called automaton-labelled formulae, which are similar to formulae of automaton propositional dynamic logic. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. We show that the known EXPTIME upper bound for regular grammar logics can be obtained using our tableau calculus. We also give an effective Craig interpolation lemma for regular grammar (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Tractable approximate deduction for OWL.Jeff Z. Pan, Yuan Ren & Yuting Zhao - 2016 - Artificial Intelligence 235 (C):95-155.
    Download  
     
    Export citation  
     
    Bookmark  
  • Complexity of hybrid logics over transitive frames.Martin Mundhenk, Thomas Schneider, Thomas Schwentick & Volker Weber - 2010 - Journal of Applied Logic 8 (4):422-440.
    Download  
     
    Export citation  
     
    Bookmark   4 citations