KL-ONE

An overview of tableau algorithms for description logics. 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 tableau procedures have been quite successful. Nevertheless, due to different underlying intuitions and applications, most description logics differ significantly from run-of-the-mill modal and program logics. Consequently, the research on tableau algorithms in description logics led to new techniques and results, which are, however, also of interest for modal logicians. In this article, we will focus on three features that play an important rôle in description logics (number restrictions, terminological axioms, and role constructors), and show how they can be taken into account by tableau algorithms.


References in zbMATH (referenced in 40 articles )

Showing results 1 to 20 of 40.
Sorted by year (citations)

1 2 next

  1. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  2. Nguyen, Linh Anh: ExpTime tableaux with global caching for hybrid PDL (2020)
  3. Baader, Franz; Borgwardt, Stefan; Peñaloza, Rafael: On the decidability status of fuzzy (\mathcalA\mathcalL\mathcalC) with general concept inclusions (2015)
  4. Borgwardt, Stefan; Peñaloza, Rafael: Reasoning in expressive description logics under infinitely valued Gödel semantics (2015)
  5. Schmidt, Renate A.; Waldmann, Uwe: Modal tableau systems with blocking and congruence closure (2015)
  6. Tao, Jia; Slutzki, Giora; Honavar, Vasant: A conceptual framework for secrecy-preserving reasoning in knowledge bases (2015)
  7. Borgwardt, Stefan; Peñaloza, Rafael: Consistency reasoning in lattice-based fuzzy description logics (2014)
  8. Glimm, Birte; Horrocks, Ian; Motik, Boris; Stoilos, Giorgos; Wang, Zhe: HermiT: an OWL 2 reasoner (2014)
  9. Schmidt, Renate A.; Tishkovsky, Dmitry: Using tableau to decide description logics with full role negation and identity (2014)
  10. Goré, Rajeev; Nguyen, Linh Anh: ExpTime tableaux for (\mathcalALC) using sound global caching (2013)
  11. Tao, Jia; Slutzki, Giora; Honavar, Vasant: PS\textscpacetableau algorithms for acyclic modalized (\mathcalALC) (2012)
  12. Baader, Franz; Peñaloza, Rafael: On the undecidability of fuzzy description logics with GCIs and product t-norm (2011)
  13. Kaminski, Mark; Schneider, Sigurd; Smolka, Gert: Terminating tableaux for graded hybrid logic with global modalities and role hierarchies (2011)
  14. Meissner, Adam: Experimental analysis of some computation rules in a simple parallel reasoning system for the (\mathcalALC) description logic (2011)
  15. Nguyen, Linh Anh; Szałas, Andrzej: ExpTime tableau decision procedures for regular grammar logics with converse (2011)
  16. Schmidt, Renate A.; Tishkovsky, Dmitry: Automated synthesis of tableau calculi (2011)
  17. Baader, Franz; Beckert, Bernhard; Nipkow, Tobias: Deduktion: von der Theorie zur Anwendung (2010) ioport
  18. Baader, Franz; Lutz, Carsten; Turhan, Anni-Yasmin: Small is again beautiful in description logics (2010) ioport
  19. Baader, Franz; Peñaloza, Rafael: Automata-based axiom pinpointing (2010)
  20. Friedmann, Oliver; Lange, Martin: A solver for modal fixpoint logics (2010) ioport

1 2 next