A heuristic skipping rules algorithm on tableau algorithm

Abstract

Ontology description can use Description Logic(DL) language, so DL's reasoning service can be used in ontology reasoning. In each kind DL, there is a corresponding tableau algorithm to do the reasoning process. There are some sophisticated software to do DL reasoning, they using tree with conflict to decide whether a problem can be using satisfiability to solve. There are a lot of optimization methods to optimize the reasoning service, their attention on the tree structure with conflict. We propose a new algorithm, Heuristic Skipping Rules Algorithm(HSRA), to simply the rule set called by tableau algorithms, and experimentally proved the effectiveness of the HSRA. © 2012 IEEE.