Introduction
Resolution is an important and attractive tool for rewriting a Description Logic
ontology into (disjunctive) datalog for the purposes of query answering [
3, 5,
6
]. This is because there are already many general purpose resolution calculi
that can support deduction in much more expressive logics and which have
well-de ned powerful redundancy elimination criteria like clause subsumption.
However, the generality of these procedures implies that the characteristics and
structure of DL axioms are not fully exploited during saturation and as a
consequence the designed rewriting algorithms often su er from performance
issues [
7, 4
]. More precisely, resolution algorithms like those designed in [
3, 5,
6
] usually produce far too many clauses that contain function terms, many
of which are never used to derive other function-free clauses that are
members of the ontology rewriting. For example, a typical algorithm will always
resolve clauses A(x) R(x; y) ^ B(y) and R(x; f (x)) C(x) to produce
A(x) C(x) ^ B(f (x)) even if the function term f (x) cannot be subsequently
eliminated.
In our previous work we have de ned a novel resolution-based rewriting
algorithm for DL-Lite and E LHI that largely avoids the generation of such
redundant clauses [
8
]. The algorithm uses a macro-inference rule, called n-shrinking,
which searches for sets of clauses such that when these are used as side-premises
in consecutive resolutions, intermediate clauses with function terms can be
produced but the nal resolvent must be function-free. For example, in the
previous scenario, the algorithm will consider resolving the two clauses to produce
A(x) C(x) ^ B(f (x)) only if a clause of the form B(f (x)) C(x) also exists
in the working set of clauses and hence the function-free clause A(x) C(x)
can nally be obtained. In order to reduce the size of the set where such pairs
of side premises are looked up, in contrast to previous approaches, the
algorithm does not \propagate" function symbols. For example, all algorithms in [
3,
5, 6
] will resolve clauses S(x; f (x)) C(x) and R(x; y) S(x; y) to produce
R(x; f (x)) C(x). In contrast, the algorithm in [
8
] will rst try to unfold the
clause R(x; y) S(x; y) on some clause of the form A(x) S(x; y) ^ B(y) to
produce A(x) R(x; y) ^ B(y) and then consider n-shrinking on that clause.
We have considerably extended our previous work and designed a datalog
rewriting algorithm for Horn-SHIQ ontologies that follows the same principles.
Our rst extension is to modify the unfolding and n-shrinking rules to be
applicable on clauses with equality that are a distinctive feature of Horn-SHIQ.
Example 1. Consider an ontology consisting of the following axioms given also
in clausal form:
A v
1R:B
D v 9R:>
C v 9S:B
S v R
y
z
R(x; g(x))
S(x; f (x))
R(x; y)
D(x)
C(x);
S(x; y)
A(x) ^ R(x; y) ^ R(x; z) ^ B(y) ^ B(z)
B(f (x))
C(x)
Unfolding between (1) and (4) produces y z A(x) ^ S(x; y) ^ R(x; z) ^
B(y) ^ B(z) on which shrinking with premises clauses (3)(a) and (3)(b) produces
f (x) z A(x)^C(x)^R(x; z)^B(z). Notice how shrinking prevents resolving
clause (1) with clause (2) which would construct a redundant resolvent.
The biggest challenge in the new algorithm is to deal with equality
reasoning. Like in [
3
] we employ superposition, however, following the ideas set in
[
8
] we try to restrict its application in such a way that unnecessary
intermediate clauses are constructed only when necessary. First, due to n-shrinking,
only equality clauses with function-free bodies can appear in the working set
(see also previous example). Hence, superposition inferences can be restricted to
have only such clauses as side premises which signi cantly reduces the search
space. However, superposition inferences can introduce new function terms in
the body of a clause. Consider for example clauses f (g(x0)) x0 B(x0) and
R(x; f (x)) A(x). The rst clause can be superposed into the second with
uni er x 7! g(x0) to obtain the resolvent R(g(x0); x0) A(g(x0)) ^ B(x0). Now,
rst, note that by the basic strategy of superposition [
1
] (superposition remains
complete if it is only applied into function terms not introduced by previous
unication steps) no subsequent superpositions need to be applied on the body of
clause R(g(x0); x0) A(g(x0)) ^ B(x0). Second, according to the ideas in [
8
] and
our previous discussion this intermediate clause is of importance only if g(x0)
can be eliminated from the body. These two observations combined imply that
we can devise the following macro-superposition inferences:
R(x; f (x))
B(f (x))
A(x) f (g(x))
R(g(x); x)
A(x) f (g(x))
B(x)
x B(x); A(g(x))
C(x) ^ B(x)
x B(x); A(g(x))
C(x) ^ B(x)
C(x)
C(x)
where f (x) has not been introduced by a previous uni cation.
A detailed description and de nition of the algorithm can be found at http:
//www.image.ece.ntua.gr/~despoina/document.pdf.
(1)
(2)
(3)
(4)
}