Extending Classical Theorem Proving for the Semantic Web.
Tanel Tammet · 2003
We investigate the applicability of classical resolution-based theorem proving methods for the Semantic Web. We consider several well-known search strategies, propose a general schema for applying resolution provers and propose a new search strategy "chain resolution" tailored for large ontologies. Chain resolution is an extension of the standard resolution algorithm. The main idea of the extension is to treat binary clauses of the general form A(x)#B(x) with a special chain resolution mechanism, which is di#erent from standard resolution used otherwise.