Tableau-Based Reasoning

Ralf Möller () and Volker Haarslev ()
Additional contact information
Ralf Möller: Hamburg University of Technology
Volker Haarslev: Concordia University

A chapter in Handbook on Ontologies, 2009, pp 509-528 from Springer

Abstract: Summary Tableau-based methods for satisfiability checking build the backbone of major contemporary ontology reasoning sytems. The main idea of tableau-based methods for satisfiability checking is to systematically construct a representation for a model of the input formulae. If all representations that are considered by the procedure turn out to contain an obvious contradiction, a model representation cannot be found and it is concluded that the set of formulae is unsatisfiable. In this chapter, tableau-based reasoning methods are formally introduced. We start with a nondeterministic basic version which subsequently will be extended with optimization techniques in order to demonstrate how practical systems can be built. We also demonstrate how computed tableau structures can be exploited for other inference problems in an ontology reasoning system.

Keywords: Description Logic; Global Constraint; Rule Application; Concept Description; Atomic Concept (search for similar items in EconPapers)
Date: 2009
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:ihichp:978-3-540-92673-3_23

Ordering information: This item can be ordered from
http://www.springer.com/9783540926733

DOI: 10.1007/978-3-540-92673-3_23

Access Statistics for this chapter

More chapters in International Handbooks on Information Systems from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().