efficiency

rules/advancedset.pl

@@ -49,13 +49,6 @@
         debug(owl2_basic_reasoner,'testing for subsumption between existential restrictions ~w ~w',[X,Y]),
         entailed(subClassOf(DX,DY),EL).
 
-entailed_2(subClassOf(X,Y),_) :-
-        (   nonvar(X)
-        ->  true
-        ;   class(X)),
-        debug(owl2_basic_reasoner,'testing for X < X^... ~w ~w',[X,Y]),
-        pairwise_equivalent_class(X,intersectionOf(DL)),
-        member(Y,DL).
 
 entailed_2(subClassOf(X,Y),_) :-
         (   nonvar(X)

rules/basicset.pl

@@ -1,4 +1,4 @@
-
+/* -*- Mode: Prolog -*- */
 
 % ----------------------------------------
 % TBox Reasoning
@@ -24,6 +24,7 @@
 entailed(subClassOfReflexive(X,Y), EL) :- entailed(subClassOf(X,Y), EL).
 entailed(subClassOfReflexive(X,X), _) :- class(X).
 
+
 entailed_2(classAssertion(C,I),EL) :-
         classAssertion(C2,I),
         debug(owl2_basic_reasoner,'testing ~w(~w) based on ~w(~w)',[C,I,C2,I]),
@@ -49,7 +50,9 @@
 
 
 % transitivity of subclass
-entailed_5(subClassOf(X,Y),EL) :- subClassOf(X,Z),\+member(X<Z,EL),entailed(subClassOf(Z,Y),[X<Z|EL]). % TODO: cycles
+% we avoid recursion by stratification - 10 cannot call a 5
+% 10 is either asserted or a precalculated set of assertions based on eg equivalentClass
+entailed_5(subClassOf(X,Y),EL) :- entailed_10(subClassOf(X,Z),EL),\+member(X<Z,EL),entailed(subClassOf(Z,Y),[X<Z|EL]). % TODO: cycles
 
 
 % subclass over existential restrictions
@@ -58,3 +61,11 @@
         subClassOf(X,someValuesFrom(P,YY)),
         subClassOf(YY,Y),
         \+ member(X<someValuesFrom(P,Y),EL).
+
+
+% e.g. if X = A and B, then treat this like X subClassOf A, X subClassOf B
+% this is v. slow when X is nonvar
+entailed_pre(subClassOf(X,Y)) :-
+        pairwise_equivalent_class(X,intersectionOf(DL)),
+        atom(X),
+        member(Y,DL).