Optimizing Reasoning with Qualified Number Restrictions in SHQ

Computational Proteomics

计算机科学;物理学

N. Farsiniamarj ; V. Haarslev

Others  :  http://CEUR-WS.org/Vol-477/paper_50.pdf
PID  :  24941

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

Using SHQ one can express number restrictions on role fillers of individuals. A typical question for a DL reasoner would be whether the concept 8hasCredit:(Science ∪Engineering t Business) u (≥120 hasCredit:(Science ∪ Engineering)) ∩ (≥ 140 hasCredit)∩(≤32 hasCredit:(SciencetBusiness))∩(≤91 has Credit: Engineering) is satisfiable. Most DL tableau algorithms [9, 1, 12] test the satisfiability of such a concept by first satisfying all at-least restrictions, e.g., by creating 260 hasCredit-fillers, of which 120 are instances of (Science ∪ Engineering). Eventually, a nondeterministic choose-rule assigns to each of these 260 individuals (Science ∪ Business) or :(Science ∪ Business), and Engineering or :Engineering. In case anat-most restriction is violated, e.g., a student has more than 91 hasCredit-fillers of Engineering, a nondeterministic merge-rule tries to reduce the number of these individuals by merging a pair of individuals until the upper bound specified in this at-most restriction is satisfied. Searching for a model in such an arithmetically uninformed or blind way is usually very inefficient.[first paragraph]