This web page categorizes n-ary rules, which refer to a finite list of elements, and present different solutions for supporting them in a rule-based system.
Contact: William Van Woensel
A first subset (L1) of n-ary rules enumerate one or more restrictions, each referring to a list element (#eq-diff2, #eq-diff3, #prp-adp, #cax-adc, #cls-uni). For instance, rule #eq-diff2 flags an ontology inconsistency if two equivalent elements of an owl:AllDifferent construct are found:
$$T(?x, type, AllDifferent), T(?x, members, ?y), \\ LIST[?y, ?z_1, ..., ?z_n], T(?z_i, owl:sameAs, ?z_j) \rightarrow false$$In contrast, rules from a second subset (L2) restrain all elements in a list (#prp-spo2, #prp-key, #cls-int1). As an example, rule #cls-int1 infers that y is an instance of an intersection in case it is typed by all intersection member classes:
$$T(?c, owl:intersectionOf, ?x), LIST[?x, ?c_1, ..., ?c_n],\\ T(?y, rdf:type, ?c_1), ..., T(?y, rdf:type, ?c_n) \rightarrow T(?y, rdf:type, ?c)$$A third ruleset (L3) yields inferences for all list elements (#cls-int2, #cls-oo, #scm-int, #scm-uni). As an example, rule #scm-uni infers that each member class of a union is a subclass of that union:
$$T(?c, owl:unionOf, ?x), LIST[?x, ?c_1, ..., ?c_n] \rightarrow\\ T(?c_1, rdfs:subClassOf, ?c), ..., T(?c_n, rdfs:subClassOf, ?c)$$In this section, we present solutions for the different types of n-ary rules.
To support rules from (L1) and (L3), list membership functions are applied. To support rules from (L2), one of the other three solutions is needed.
The following two rules infer list membership; i.e., they link each list element (indicated by rdf:first) to all preceding list cells (i.e., blank nodes making up the linked list), meaning that the first cell will be directly linked to all list elements.
$$T(?l, first, ?m) \rightarrow ?T(?l, hasMember, ?m)\\ T(?l_1, rest, ?l_2), T(?l_2, hasMember, ?m) \rightarrow T(?l_1, hasMember, ?m)$$Using these two rules, rules from (L1) and (L3) can be supported. As an example, using these rules, #scm-uni (L3) may be represented as follows:
$$T(?c, unionOf, ?l), T(?l, hasMember, ?cl) \rightarrow T(?cl, subClassOf, ?c)$$Since the list membership rules link each list element (in this case, union member class) to the first list cell $?l$, the rule will yield inferences for all member classes of the union.
Based on relevant n-ary assertions from the ontology, this solution instantiates rules from (L2). In particular, an OWL2 RL rule is instantiated for each relevant n-ary assertion (e.g., propertyChainAxiom for rule #prp-spo2), leading to multiple instantiated rules per original rule. E.g., a property chain axiom P with constituent properties P1-P3 will yield the following rule:
$$T(?u_1, P_1, ?u_2), T(?u_2, P_2, ?u_3), T(?u_3, P_3, ?u_4) \rightarrow T(?u_1,P,?u_4)$$In related work, this kind of instantiation (or "rule-templates") approach is applied for any n-ary rule [1] or even for all (instance-based) OWL2 RL rules [2, 3, 4]
Normalize (or "binarize") the input ontology to only contain binary versions of n-ary assertions relevant to (L2). For instance, an n-ary intersection can be converted to a set of binary intersections as follows:
$$I = C_1 \cap C_2 \cap ... \cap C_n \equiv \\ I = C_1 \cap I_1 \wedge I_1 = C_2 \cap I_2 \wedge ... I_{(n-2)} = C_{(n-1)} \cap C_n$$The binary version of rule #cls-int1 looks as follows:
$$T(?c, intersectionOf, ?x_1), T(?x_1,first,?c_1), T(?x_1,rest,?x_2),T(?x_2,first,?c_2 ),\\ T(?y, type, ?c_1), T(?y, type, ?c_2) \rightarrow T(?y, type, ?c)$$This rule may be considered recursive, since it both references and infers the same kind of assertion (i.e., T(?y, type, ?c)). It is not hard to see how this approach only works for recursive rules, since it relies on producing partial inferences to generate the final inference. Rule #prp-key is not a recursive rule, since it infers equivalence between resources but does not refer to such relations. Consequently, this approach only works for rules #prp-spo2 and #cls-int1 from (L2).
Replace each n-ary rule by 3 auxiliary rules
Replace each rule from (L2) by 3 auxiliary rules. Bishop et al. [5] suggested this solution for OWLIM, based on a W3C note [6]. We show the auxiliary rules for #cls-int below:
$$T(?l, first, ?c), T(?l, rest, nil), T(?y, type, ?c)\\ \rightarrow T(?y, inIntersection, ?l)\\ \\ T(?l, first, ?c), T(?l, rest, ?l_2), T(?y, type, ?c), T(?y, inIntersection, ?l_2) \\ \rightarrow T(?y, inIntersection, ?l)\\ \\ T(?x, intersectionOf, ?l), T(?y, inIntersection, ?l) \rightarrow T(?y, type, ?x)$$In this solution, a first auxiliary rule starts at the end of any list ($T(?l, rest, nil)$ ), and infers an intermediary assertion for the last element (cell n). Starting from the first inference, a second rule travels up the list structure ($T(?l, rest, ?l_2)$ ) by inferring the same kind of assertions for cells n-1 up until cell 1. In case the first cell is related to the relevant assertion (e.g., intersection, property chain or has-key), a third auxiliary rule generates the original, n-ary inference.