3

这是 builtin_owl2-rl.pie 第 361 行

// Part 1 of cls_oo
Id: cls_oo_1
     c <owl:oneOf>    x
     ------------------
     c <onto:_oneOf>  x                     [Context <onto:_cls_oo>]


// Part 2 of cls_oo
Id: cls_oo_2
     c  <onto:_oneOf>  x                    [Context <onto:_cls_oo>]
     x  <rdf:first>    y
     x  <rdf:rest>     z
    -------------------------------
     y  <rdf:type>     c
     c  <onto:_oneOf>  z                    [Context <onto:_cls_oo>][Constraint z != <rdf:nil>]

一些随机的东西来安抚stackoverflow的“AI”建议“这只是代码，添加解释”

4

1 回答 1

1

此规则实施https://www.w3.org/TR/owl2-profiles/#cls-oo。

  • owl:oneOf是原始财产；它的对象是一个列表。
  • onto:_oneOf是用于展开列表的实现属性。它总是放在一个实现上下文中onto:_cls_oo。永远不应返回来自此上下文的三元组。

现在想象你得到了c owl:oneOf (y1 y2)这真的意味着

c owl:oneOf [rdf:first y1;
         rdf:rest [rdf:first y2;
                   rdf:rest rdf:nil]]

第一条规则将其复制到onto:_oneOf. 然后第二条规则产生

y1 rdf:type c.
c onto:_oneOf [rdf:first y2; 
               rdf:rest rdf:nil]]

第二条规则再次启动并产生

y1 rdf:type c.
y2 rdf:type c.
c onto:_oneOf rdf:nil

前两个是你想要推断的，第三个是隐藏在实现上下文中的剩余部分。

你得到这个了吗？如果你这样做了，试着证明owl:propertyChainAxiom https://www.w3.org/TR/owl2-profiles/#prp-spo2的实现是正确的：

Id: prp_spo2_1
    p <owl:propertyChainAxiom> pc
    start pc last                   [Context <onto:_checkChain>]
    ----------------------------
    start p last

Id: prp_spo2_2
    pc <rdf:first> p
    pc <rdf:rest> t                 [Constraint t != <rdf:nil>]
    start p next
    next t last                     [Context <onto:_checkChain>]
    ----------------------------
    start pc last                   [Context <onto:_checkChain>]

Id: prp_spo2_3
    pc <rdf:first> p
    pc <rdf:rest> <rdf:nil>
    start p last
    ----------------------------
    start pc last                   [Context <onto:_checkChain>]
于 2017-01-13T19:40:44.890 回答