A connection tableau reasoner for Description Logics
|has title::Approximations of Connection Tableaux for the Description Logic ALC|
|Master:||project within::Knowledge Technology and Intelligent Internet Applications|
|Student name:||student name::Ruben Weber|
|Supervisor:||Stefan Schlobach, Szymon Klarman|
|Second reader:||has second reader::Zhisheng Huang|
The tableau method is a proof procedure that is often used in the field of automated reasoning. However, without optimizations it is too inefficient for many practical tasks. The size of the proofs can grow exponentially. In this thesis we present a way of improving the tableau efficiency for description logic ALC. The presented methods are based on the connection condition, a technique that brings structure into the tableau reasoning and improves efficiency, but that is not directly applicable to description logic tableaux. We propose four methods, each one putting additional constraints on the tableau reasoning. All methods are proven to be sound and terminating, two methods are proven to be complete. Apart from the methods themselves, we present results of practical experiments with implementations of the methods and an implementation of a standard tableau algorithm. The methods are tested on both benchmark knowledge bases and real-life knowledge bases. By means of an analysis of the results we show that the benefits of the proposed connection methods easily outweigh the efforts.