Semantic locality implementation is incorrect. What it should do it to take an axiom, replace all the entities not in signature with top/bottom entities of a kind and check whether the reasoner entails this new axiom. In FaCT++ I have to follow the root it is currently implemented because there is no isEntailed() interface there. Also this implementation misses the axiom transformation bit, which in FaCT++ is hidden in class TExpressionTranslator. I might implement this at some point but I'm not sure when I'll have time.
Semantic locality implementation is incorrect. What it should do it to take an axiom, replace all the entities not in signature with top/bottom entities of a kind and check whether the reasoner entails this new axiom. In FaCT++ I have to follow the root it is currently implemented because there is no isEntailed() interface there. Also this implementation misses the axiom transformation bit, which in FaCT++ is hidden in class TExpressionTranslator. I might implement this at some point but I'm not sure when I'll have time.