Tableau-Based Reasoning

Abstract

Tableau-based methods for satisfiability checking build the backbone of major contemporary ontology reasoning systems. 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.