Closed fcbr closed 5 years ago
This formula:
(=> (exhaustiveDecomposition ?CLASS ?ROW0 ?ROW1) (and (instance ?CLASS Class) (instance ?ROW0 Class) (instance ?ROW1 Class)))
was relativized as:
(forall (?CLASS ?ROW1 ?ROW0) (=> (and (instance ?ROW0 Entity) (instance ?ROW0 Class) (instance ?ROW1 Entity) (instance ?ROW1 Class) (instance ?CLASS Class) (instance ?CLASS Entity)) (=> (exhaustiveDecomposition3 ?CLASS ?ROW0 ?ROW1) (and (instance ?CLASS Class) (and (instance ?ROW0 Class) (instance ?ROW1 Class))))))
Which is clearly wrong: the purpose of the formula is to instantiate ?CLASS, ?ROW0, and ?ROW1 as instances of Class, so they can't be added as restrictions in the antecedent.
?CLASS
?ROW0
?ROW1
Class
Can we generalize it so all (instance ...) in the conclusion of the rules should not contribute to types restrictions ?
Yes, that's the idea.
Close in favor of #24. Same issue.
This formula:
was relativized as:
Which is clearly wrong: the purpose of the formula is to instantiate
?CLASS
,?ROW0
, and?ROW1
as instances ofClass
, so they can't be added as restrictions in the antecedent.