Skip to content
Commit 397df58f authored by Christoph Schwering's avatar Christoph Schwering
Browse files

Fixed: order of splits matters for Solver::Determines().

For Determines(), the split order matters, for Entails() it does not.
Suppose we have two split terms t1, t2, t3 and two names n1, n2, and
a query term t and two candidate names n, n' for t.

Let us assume that for all combinations of t1=N*, t3=N**, the reasoner
finds that t=n.

The reasoner splits t1 at the first level, and after setting t1=n1 it
descends to the next split level, where it successfully splits t2, which
obtains t=n' as binding for t. Back at split level one, the reasoner now
considers the case t1=n2, again descends to the next level, where it
splits, say, t3, and obtains t=n.

Back at split level one, the reasoner sees that t=n' and t=n are
incompatible and hence proceeds by splitting t2, which does not succeed.
In a way, t=n' found with t2 after t1=n1 blocks the real solution.

Again at level one, the reasoner splits t3. If the order does not
matter, it will not descend to any further split level, since all
unordered combinations of t1, t2, t3 have been tested already.

If the order does matter, however, it does descend to the next level.
There it will split t1: even if it picks t2 before t1, t2 will prove
incompatible with t3 (*). And once it splits t1 at level two, it will
find t=n, which this time is not blocked by t=n'.

(*) This holds under the assumption that the KB is consistent.
If the KB is not consistent, could split terms 'block' each other?
parent 85511d58
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment