A connection tableau reasoner for Description Logics

From Master Projects
Jump to: navigation, search

has title::Approximations of Connection Tableaux for the Description Logic ALC
status: ongoing
Master: project within::Knowledge Technology and Intelligent Internet Applications
Student name: student name::Ruben Weber
number: student number::1561278
Start start date:=2010/02/01
End end date:=2010/08/01
Supervisor: Stefan Schlobach, Szymon Klarman
Second reader: has second reader::Zhisheng Huang
Poster: has poster::Media:Media:Posternaam.pdf

Signature supervisor



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.