Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

蕴涵

purrdf-entail(重新导出为 purrdf::entail)是面向 PurRDF RdfDataset IR 的原生、wasm32-clean(可干净构建到该目标)的蕴涵实现。一组引擎位于同一个门面之后,每个引擎都是其对应 SPARQL 蕴涵机制(entailment regime)的合适工具——完全在驻留的 TermId 空间中把数据集闭合到其推理得出的不动点,不依赖外部推理机,不依赖异步运行时,也不做字符串往返。

接口一览

入口蕴涵机制引擎
materialize(ds, regime)Simple、RDF、RDFS、OWL-RL、D通过原生的半朴素不动点,对该机制所声明的子句程序进行前向物化(「chase」)。返回 (closure, ReasoningReport);报告不是可选的。
materialize_dl_reported(...),或 materialize(ds, Materialization::OwlDirect(bgp))OWL-Direct基于 SHOIQ(D) tableau(表算法)的开放世界 OWL DL,由查询的基本图模式 bgp 引导;对于该机制,materialize 委托给它,而不是重新表述一遍。
materialize_rif(...)RIF在已解析的 RuleSet 上进行 RIF-Core 规则蕴涵。
parse_rif_xml(...) / resolve_rif_imports(...)RIFRIF-XML 解析,导入解析由调用方持有且不涉及 I/O。
rules(regime) / implemented(regime)—某一机制_据以定义_的规则表,以及本工作区实际触发的子集。二者之差就是可度量的差距。
calculus_program(regime)—该机制的演算,以 DL 子句数据的形式给出——正是 materialize 所求值的那个程序,因此使用方可以重新计算其契约哈希。
Regime::from_iri(iri)—把 sparql:entailmentRegime IRI 解析为对应的枚举值。
#![allow(unused)]
fn main() {
use purrdf::entail::{materialize, Completeness, Materialization};

let ds = purrdf::parse_dataset(
    b"<https://example.org/alice> <https://example.org/name> \"Alice\" .",
    "application/n-triples",
    None,
)?;
// 把冻结的数据集闭合到其 RDFS 不动点;结果是一个新的数据集,
// 以及一份说明本次运行做了什么的报告。
let (closed, report) = materialize(&ds, Materialization::Rdfs).expect("materializes");
assert_eq!(report.completeness(), Completeness::ExactWithinBoundaries);
assert!(closed.quad_count() > ds.quad_count());
Ok::<(), Box<dyn std::error::Error>>(())
}

同一个引擎,五种宿主

蕴涵并不按宿主各自重新实现。purrdf 命令行、Python、WebAssembly 与 C ABI 都经由同一个共享的字符串边界(purrdf_validate::regime)调用 Rust 引擎,各个接口都对照同一份已提交的黄金向量工件进行检查——因此一旦出现分歧,表现为某一个向量失败,而不是几个接口悄无声息地不再一致。机制的拼写(simple、rdf、rdfs、owl-rl、owl-direct、rif、d)在各处都相同。

宿主物化定义的规则表已实现的规则
Rustmaterialize(&ds, Materialization::Rdfs)rules(Regime::Rdfs)implemented(Regime::Rdfs)
CLIpurrdf reason --regime rdfs、purrdf convert --entailment rdfs、purrdf query --entailment rdfs(purrdf entails 则提出以结论为导向的问题)——
Pythonpurrdf.entail.materialize(dataset, "rdfs", "", imports, premise_iris)、purrdf.entail.materialize_nt(text, "rdfs", "", imports, premise_iris)purrdf.entail.rules("rdfs")purrdf.entail.implemented_rules("rdfs")
JavaScript / WebAssemblyentailMaterialize(doc, "rdfs", "", iris, docs, premiseIris)entailRules("rdfs")entailImplementedRules("rdfs")
Cpurrdf_entail_materialize_to_nquads(...)purrdf_entail_rules(...)purrdf_entail_implemented_rules(...)

每个宿主都能物化每一种机制;没有任何宿主拒绝其中之一。有两种机制需要的是一项「输入」,而每个宿主都为此提供了参数:CLI 上的 --rules <FILE>,Python、WebAssembly 与 C 接口上的 program 字符串,以及 Rust 中的 Materialization 值本身。rif 在这里接收一份规范性的 RIF-in-XML 规则文档;其他机制都不接收规则文档,若提供则是错误,而不是一个被丢弃的参数。owl-direct 的额外输入是一个_查询_的类表达式,因此「文档进、文档出」的调用运行的是与查询无关的增强,而查询接口(purrdf::query_with_entailment、purrdf query --entailment owl-direct)才是查询导向通道所在之处。

一条宿主相关的说明:

  • WebAssembly 模块还导出 entailCheckGoldenVectors(),它在使用方实际加载的那个模块内部重放已提交的三宿主向量工件——因此无需信任本仓库的 CI,就能检查与参考实现是否一致。

换一种问法:以结论为导向的服务

物化回答的是「这个前提蕴涵什么?」。下面三个服务回答的是「这个前提是否蕴涵_那个_?」,这是另一个问题,而不是它看起来那样在推理闭包中做成员测试:结论中的空节点是必须被_映射_的存在量词,不相容的前提蕴涵一切,找不到映射并不说明任何问题,除非规则集对其所运行的前提是完备的——而且一个结论可以被蕴涵,却根本不出现在闭包中,这正是规则表之外那五种判定手段(mechanism)存在的原因(参见一致性)。

它们运行在同一个共享边界之上,覆盖全部五种宿主形态,purrdf 命令行即其中之一。scripts/check-entailment-surface.py 是把关的检查:它从 purrdf-entail 自身的公共入口推导出服务集合,并且只要其中任何一个服务无法_带着边界的完整参数列表_从每个宿主到达,检查就失败,因此一个服务或一个参数不可能只落地到四个宿主而在第五个上缺席。它还会在每次运行时对自身做变异测试——每项检查一处编辑,在内存中施加于已提交的代码树,每一处都必须使该检查失败——因为一项无法拒发绿灯的检查就不算检查。

宿主P 是否蕴涵 C?重新判定蕴涵证据(warrant)模式的确定答案(certain answers)
Rustentails(&p, &c, Regime::OwlRl, &imports)verify(warrant, &p, &c)certain_answers(&p, &bgp, Regime::OwlRl, &imports)
CLIpurrdf entails --regime owl-rl --premise P --conclusion C… --conclusion C --verify… --pattern BGP
Pythonpurrdf.entail.graph_entails("owl-rl", p, c, imports, premise_iris)purrdf.entail.verify_entailment(...)purrdf.entail.certain_answers("owl-rl", p, bgp, imports, premise_iris)
JavaScript / WebAssemblyentailGraphEntails("owl-rl", p, c, iris, docs, premiseIris)entailVerifyEntailment(...)entailCertainAnswers(...)
Cpurrdf_entail_graph_entails(...)purrdf_entail_verify_entailment(...)purrdf_entail_certain_answers(...)

与上面的物化表相比有两点不同,二者都源于所提出的问题,而非任何宿主:

  • 五种机制,而不是七种。 owl-direct 由_查询_的类表达式引导,rif 在_调用方_的规则文档下进行蕴涵,而「前提、结论、机制」两者都不携带。二者在每个宿主上都会被点名拒绝——绝不会在较弱的机制下作答并贴上所请求机制的标签——而二者仍然可以物化。
  • 导入表在每个宿主上都是参数。 本体的导入闭包_就是_该本体,因此,若前提携带了一条调用方没有交给本次调用的 owl:imports,它就已是另一个前提。PurRDF 不获取任何内容,因此导入闭包以调用方提供的配置形式到达:一个有序的 (本体 IRI, 文档) 配对列表,在命令行上写作 --import IRI=FILE。当某个导入指向前提文档本身时无需配对——在 CLI 上是 file:// 获取 IRI 或 --base,在 Python、WebAssembly 与 C 宿主上是 premise_iris 参数(JavaScript 中为 premiseIris),即调用方读取前提所用的 IRI,裸文本则为 []——指向前提中已有的图(<X> a owl:Ontology、<X> a sh:ShapesGraph,或某个 owl:versionIRI 指名它)时,同样无需配对。其他任何未解析的导入都会以点名该文档的方式被拒绝,绝不会成为一个被静默截断的前提;前提的闭包从未到达的导入表条目同样会被拒绝——它会被读取,却从未被使用——在每个宿主上都是如此,正如 SHACL 验证会拒绝未被使用的形状图条目。其他每一个蕴涵服务都接受同一张表并施加同一条规则:物化(CLI reason、convert --entailment;Python materialize/materialize_nt;WebAssembly entailMaterialize;C purrdf_entail_materialize_to_nquads;Rust materialize_with_imports)、蕴涵机制查询(CLI query --entailment … --import IRI=FILE;Python Store.query_entailment_governed(..., imports=…, premise_iris=…);WebAssembly queryEntailmentGoverned 的 importIris/importDocuments/premiseIris 选项;C purrdf_query_entailment_governed 的 import_iris/import_documents/ import_count;Rust query_with_entailment_closure_governed),以及 OWL-Direct 相容性问题(CLI consistency --import IRI=FILE;Python consistency(data, imports, premise_iris);WebAssembly entailConsistency(doc, iris, docs, premiseIris, …);C purrdf_entail_consistency)。每一个服务都对合并后的前提求闭包或作出判定,在其报告或证书中声明 ontology-import-resolved,并完全像 reason 那样拒绝未解析的导入或未被到达的条目。不接受导入表的 Rust 入口点(query_with_entailment、query_with_entailment_governed)以空表进行解析,因此导入了自身不持有的文档的前提在那里同样会被拒绝,绝不会在缺少该文档的情况下求闭包。所读取的 owl:imports 与 SHACL 验证所读取的相同:位于前提自身的 IRI 上、owl:Ontology 头上、sh:ShapesGraph(包括 sh:RulesGraph 及其子类)上,或以其中之一作为其 owl:versionIRI 的节点上。任何其他节点上的 owl:imports(包括仅为 sh:DataGraph 的节点)都是普通的前提三元组。

模式是在任意位置(包括谓词位置)带有 ?name(或 $name)的 N-Triples。RDF 把该位置保留给 IRI,因此边界的做法是:把每个变量改写为取自某个命名空间的项(该命名空间由边界扫描调用方自己的文本后划出),之后再把每次出现映射回来;该命名空间的任何内容都不会出现在结果行、绑定或报告中。唯一不接受变量的位置是字面量的数据类型:"5"^^?d 要求在一个存放 IRI 而非项的位置上进行绑定,它会被点名拒绝——替身绝不能留在那里,否则它匹配的是边界自己的命名空间,而不是调用方的数据。谓词变量与其他变量一样被投影;在 owl-rl 下,它还会产生一个 limit:它的取值范围是整个谓词词汇表,因此也涵盖 schema 谓词,而规则表的完备性所依据的定理并不覆盖这些谓词。该定理是 OWL 2 Profiles §4.3 中的定理 PR1,其假设分为两半:前提处于 OWL 2 RL 语法之内,且结论是_断言型_的——即基于类名的类断言、属性断言,以及基于具名个体的 owl:sameAs 与 owl:differentFrom。只有两半同时成立时规则表才是完备的,因此对于 schema 结论,无论 scm-* 是否推出了它,规则表都不声称完备。谓词变量还涵盖由规则表之外的判定手段所判定的构造,而结果行所取自的推理闭包对这些构造不含任何内容。

每个答案都附带其背后那次运行的证书——与物化所输出的相同的 purrdf-reasoning-report 块,外加一行 mechanism,指明是六种判定手段中的哪一种得出了裁决。

规则覆盖

rules(regime) 是规范用来定义该机制的规则表;implemented(regime) 是求值器实际触发的子集。二者都是按规范表格顺序排列的 &'static 切片,因此差距是一个可执行的工件,而不是一句话:

机制规则表定义数已实现
Simple—(恒等闭包)00
RDFRDF 1.2 Semantics §8.1.133
RDFSRDF 1.2 Semantics §8.1.1 + §9.2.11818
OWL-RLOWL 2 Profiles §4.3 表 4–97878
DOWL 2 Profiles §4.3 表 855
OWL-Direct—(SHOIQ(D) tableau,而非固定的表)00
RIF—(调用方提供的规则集)00

逐条规则的明细——每个规则 id、其规范出处,以及是否触发——是由该 API 生成的,并受漂移防护,因此不会落后于代码。

数字止步之处:

  • 四条存在性规则会触发,但其结论被扣留。 rdfD1、rdfD1a、rdfs14 与 rdfs14a 各自得出关于一个_新_空节点的结论。受限 chase 为每个这样的空节点生成一个以前沿为地址的 Skolem 见证,并在其上求闭包,因此这些规则确实会触发——但在把闭包物化回来时,每个提及替代项(surrogate)的结论都会被丢弃,因为 SPARQL 蕴涵机制从作用域图(scoping graph)中取答案,而替代项不在其中。这种扣留以 Construct::Surrogate 报告。不含替代项的内容不会丢失:把一个项替换为新的空节点只会削弱一个三元组。
  • 完整的规则表并不等于完整的推理闭包。 OWL-RL 触发全部 78 条规则,而一次遇到边界的运行仍然报告 Completeness::ExactWithinBoundaries,而不是 Exact。这两项声明是有意分开报告的。完整的规则表也不等于蕴涵一致性:在本仓库随库固化的 W3C OWL 2 RL 蕴涵测试语料上,entails() 到达了已发布的 27 个正向蕴涵中的 27 个,并在 23 个负向蕴涵中的 23 个上与 W3C 一致——这 23 个中有 3 个被_驳倒_(判定为非蕴涵),20 个被_接纳_(计算出推理闭包并观察到其中不含该非结论)。23 of 23 应读作「未发现不可靠性」,绝不能读作「证明了 23 个非蕴涵」(参见下文一致性)。78 / 78 表示表 4–9 中的每条规则都已实现——而 W3C 发布的蕴涵中唯一一个只能由这些表之外的某条可靠规则到达的,是由一个扩展 ext-eq-diff-sym 到达的:extensions(Regime::OwlRl) 列出了它,rules() 与 implemented() 都不列出它,每份报告都在单独的 extension 行中输出它。另有八个是通过反驳而非匹配到达的,这些根本不增加任何规则:参见下文的一致性一节。
  • 有十七条 OWL 2 RL 规则的结论是 false。 对这些规则而言,「已实现」意味着_已判定_:规则体一旦匹配,就成为 EntailError::Inconsistent,并携带一个见证,指明该规则以及满足它的那些断言三元组。对一条没有结论的规则而言,这是它唯一能做的事。

chase(Simple / RDF / RDFS / OWL-RL / D)

materialize 运行一次前向物化 chase:为所选机制准备一个固定规则集,以半朴素不动点方式施加,直到不再出现新的四元组为止。由于它运行在冻结的 IR 上,它是确定性的——给定的输入与机制总是得出相同的推理闭包——又由于它在 TermId 空间中工作,途中没有任何项会被重新解析或重新序列化。

典型用法:先物化,然后用普通的 SPARQL 引擎查询,或用 SHACL 验证推理闭包(SHACL 验证器本身不做任何推理)。

规则集不会被写两遍。calculus_program(regime) 把它输出为 DL 子句,而 materialize 正是通过 purrdf-datalog 的半朴素求值器对这些子句求值,因此报告所携带的契约哈希标识的就是实际运行的子句。

RDF、RDFS、OWL-RL 与 D 通道在 purrdf-datalog 的求值上限下运行:每个图的存储可持有的事实,以及其规则可枚举的候选解。默认值在原生环境下为 4,194,304 条事实与 1,048,576 个连接步,在 WebAssembly 中为 131,072 与 1,048,576。需要其他上限的调用方需声明它们——Rust 中为 materialize_with(ds, plan, &options, stop),purrdf reason 与 purrdf convert --entailment 上为 --max-stored-facts 与 --max-join-steps,Python 的 materialize 与 materialize_nt 上为 max_stored_facts= 与 max_join_steps=,entailMaterialize 上为 maxStoredFacts 与 maxJoinSteps,purrdf_entail_materialize_to_nquads 上为 max_stored_facts 与 max_join_steps。越过上限的运行会被拒绝,并点名该上限、相关数值以及该宿主上的参数;在上限之内的运行返回的推理闭包,与任何更大上限下的完全相同,其报告的契约哈希指名的是所生效上限下的演算。

其他每一个对某个蕴涵机制的规则表求值的服务,都接受同样的两个上限,并点名调用方所调用的那个入口点上的参数——绝不会向无从触及 Rust 类型的调用方点名一个 Rust 类型。以结论为导向的服务用它们约束前提的推理闭包,以及反驳与冻结机制的每一次重新 chase:Rust 中为 entails_with 与 certain_answers_with(字符串边界上为 MaterializeLimits),purrdf entails 上为 --max-stored-facts 与 --max-join-steps,Python 的 certain_answers、graph_entails 与 verify_entailment 上为仅限关键字的 max_stored_facts= 与 max_join_steps=,entailCertainAnswers、entailGraphEntails 与 entailVerifyEntailment 上为末尾的 maxStoredFacts 与 maxJoinSteps,三个 C 入口点上则为位于 premise_iri_count 之后的 max_stored_facts 与 max_join_steps。蕴涵机制查询用它们约束自身的推理闭包:Rust 中为 EntailmentClosure::with_limits,purrdf query --entailment 旁为 --max-stored-facts 与 --max-join-steps,Store.query_entailment_governed 上为 max_stored_facts= 与 max_join_steps=,queryEntailmentGoverned 上为 maxStoredFacts 与 maxJoinSteps 选项,purrdf_query_entailment_governed 上则为这两个参数;查询 governor 仍然只为在推理闭包上的求值计价。OWL-Direct 相容性问题不运行任何规则表:其求值器是 hypertableau,在每个宿主上都受 step_cap 与 work_cap 约束,因此它不接受任何存储事实或连接步参数——那样的参数什么也约束不了。

每次运行都说明它做了什么

materialize 返回 (closure, ReasoningReport)。刻意不提供不带报告的变体,因为另一种做法——两个入口,其中一个丢弃证据——正是部分规则集被描述成完整规则集的由来。报告包含:

  • Completeness——由 rules(regime) 减去 implemented(regime) 得出,因此随着规则的加入会自行改善,并且它点名列出 missing 规则,而不只是计数;
  • 逐规则触发计数——哪些规则触发了,各自贡献了多少结论;
  • Boundary——本次运行遇到且无法闭合的构造,各附原因;
  • 求值预算——本次运行在其所处的求值上限下消耗了多少;
  • 契约哈希——purrdf-datalog 对子句程序及所生效求值上限的摘要,因此在另一种演算下、或在不同上限下生成的缓存推理闭包可以被_拒绝_,而不是被信任;
  • 不相容见证,当一条结论为 false 的规则匹配时给出:规则 id、按前提顺序满足其前提的断言三元组,以及它们所取自的图。

报告不可能在列出边界的同时声称 Exact。ReasoningReport 根本不存储完备性字段:completeness() 从边界列表本身推导出该值,因此矛盾的状态不可表示,而不只是被检查。这是有意为之——早先的设计存储了该字段,并把它与对同一组输入的推导结果相比较,这在构造上就是空洞的,永远不可能失败。

输出是字节稳定的,因此对于相同输入,Python、WebAssembly 与 C 宿主返回的报告文本与 Rust 相同。

OWL-Direct:tableau

OWL-Direct 语义是开放世界的描述逻辑,前向 chase 无法回答。materialize_dl_reported 改为运行一个 SHOIQ(D) tableau(表算法)——通过分类、实现(realization)与查询导向的物化来回答实例查询与包含(subsumption)查询。由于它需要查询的类表达式,它把这些表达式作为自己的 query_bgp 参数接收;materialize 对 Materialization::OwlDirect 委托给它,从而到达同一个 tableau,而不是重新表述它。

RIF

materialize_rif 在已解析的 RuleSet 上求值 RIF-Core 规则,覆盖 SPARQL RIF 蕴涵机制。

D(数据类型)蕴涵

D 会被物化,而不是被拒绝。PurRDF 把它实现为 Simple 蕴涵加上 OWL 2 Profiles §4.3 表 8 中的五条 dt-* 规则——即前向 chase 能为其枚举的固定规则表——由 purrdf-xsd 在 XSD _值_空间上判定,而不是通过比较词法形式。

表 8 未覆盖的是无限的值空间本身,这一点作为本次运行的 Construct::DatatypeValueSpace 边界被报告,而不是被声称已覆盖。因此 D 推理闭包是_在其所陈述的边界之内_完备的,而报告正是陈述该边界的地方。

每个宿主都能物化 d,命令行工具也不例外。

不存在「不支持的机制」错误。materialize 接收一个 Materialization,它携带每种机制各自的输入——OWL-Direct 是一个基本图模式,RIF 是一个 RuleSet——因此该类型的七个变体分别交给对应引擎处理。无效输入、不相容及资源上限耗尽会返回带类型的错误。Regime 仍然是报告与标识所用的类型,ReasoningReport::regime()、rules()、implemented() 与 Regime::from_iri 都以它表述。

不变量

  • 不生成任何词汇。 该 crate 的 vocab 模块中的每个常量都是取自蕴涵规范本身的标准 rdf:/rdfs:/owl: IRI——按照工具包而非本体的规则,该 crate 不编造任何词汇。
  • 依赖精简且 wasm-clean。 依赖项为 purrdf-core、purrdf-datalog、purrdf-xsd、purrdf-lex、purrdf-iri、purrdf-hash,以及以 purrdf-core 的固定密钥哈希器为键计算哈希值的 hashbrown 原始哈希表——每一个都是 wasm32-unknown-unknown-clean(可干净构建到该目标),因此这些引擎可以原样带入 Rust、Python、WebAssembly 与 C,不依赖线程、文件系统或 RNG。
  • 确定性。 相同的输入 + 机制 → 相同的推理闭包,始终如此——报告也逐字节相同。

一致性

两份语料度量的是两件不同的事,这一区别很重要:

  • W3C SPARQL 1.1 蕴涵机制测试组——70 个用例中 70 个通过,台账中残余为零:RDF/RDFS/OWL-RL chase、OWL-Direct(DL)tableau、RIF-Core 规则引擎,以及 RDF 公理性的谓词类型推定,全部经由 SPARQL 一致性测试框架运行。

  • W3C OWL 2 测试套件——262 个用例中 262 个裁决一致,0 例入台账,未入台账者为零。这份语料是_相容性_(consistency)形态的:全部 262 个随库固化的用例都是 otest:ConsistencyTest(226 个)或 otest:InconsistencyTest(36 个)。因此它评判的是 DL/tableau 通道的可满足性裁决,对 OWL 2 RL 规则表则什么也没有说明。带类型的台账包含 0 个分歧。每一个分歧和每一条过时的台账条目仍会导致硬失败。

    这一行没有说明的有两点。第一,上游材料并非不含蕴涵测试——W3C 清单中有 206 个正向与 23 个负向蕴涵测试;这份语料缺少它们,是因为它所取自的扁平化版本提取了前提字面量而丢弃了结论字面量,而后者恰恰是蕴涵评分所需的那一半。它们已随库固化,并由下一条目评分。第二,这份语料是一个子集:上游 482 个相容性形态用例中的 262 个。在它排除的 220 个中,有 172 个在测量排除情况时被 tableau 判定(108 个相容,64 个不相容),0 个在 40 s 上限内未终止,25 个被扣留(20 个因推理机,5 个因解析),23 个不带 RDF/XML 前提——因此这种排除是对载荷的分拣,而非能力限制,而「262 个中 262 个」是基于一份语料的数字,而不是基于 W3C 所发布内容的数字。

    这五个数字是一次注明日期的测量,记录在 census.tsv 的 dl_probe 列中,并在该套件的 PROVENANCE.md 中说明。测试框架读取该列,并在每次运行时打印出来;它并不会对被排除的 220 个用例重新运行推理机,因此这一行无法发现其中的回归。重新推导这些数字意味着重新运行探测,这是一项有意的操作,而不是把关检查的一部分。

  • W3C OWL 2 RL 蕴涵测试——50 个用例中 50 个一致,0 例入台账,未入台账者为零。这是规则表的独立判定依据(oracle):W3C 自己的蕴涵测试,每个用例在 Regime::OwlRl 下调用一次 purrdf_entail::entails() 作答。两个通道证明的是不同的事,分开报告。

    负向通道为 23 个中 23 个:无不可靠性。 chase 从未推出任何 W3C 公布为_不_被蕴涵的三元组。这是安全性结果,它在_全部_ 23 个负向用例上都成立——可靠性是每个用例都必须满足的,因此没有按 profile 过滤任何用例。

    这 23 次一致是两种不同的结果,测试框架会打印其划分,单独占一行记分板:

    OWL2-RL-NEGATIVE: total 23 = refuted 3 + admitted 20 (premise-outside-rl 5, conclusion-outside-rl 10, construct-not-read 5, refutation-budget 0, freeze-budget 0, data-range-containment 0) + unsound 0 + withheld 0
    

    其中三个是_已判定_的非蕴涵——定理 PR1 假设的两半都成立,因此推理闭包不含该非结论即构成证明。其余 20 个是_接纳_:推理闭包已计算,且不含该非结论,这就是可靠性观察的全部,除此之外不作任何声明。两者都一致,而且理应如此;它们的区别在于鉴别力,因为一个什么也推不出的推理机同样会得到 negative 23 of 23,只是 refuted 0。23 of 23 应读作「未发现不可靠性」,绝不能读作「证明了 23 个非蕴涵」。

    正向通道为 27 个中 27 个——W3C 自己在基于 RDF 的语义下归入 RL profile 的 27 个正向蕴涵——而带类型的分歧台账 purrdf_sparql_conformance::owl2_rl::LEDGER 为空(EMPTY)——schema-conclusion 为 0,negative-conclusion 为 0,construct-outside-rl 为 0,imports-unresolved 为 0,且需要采取行动的项为 0(missing-rule 为 0)。

    它过去包含的每一类都已关闭,而为了关闭其中任何一类,规则表一次也没有改变。entails() 以六种方式得出结论,其中五种不是匹配:

    • 反驳。 表 4–9 中仍然没有任何规则以否定事实为规则头——没有规则得出 owl:differentFrom,也没有规则得出属于某个 owl:complementOf 类的成员关系。该表_确实_拥有的是十七条结论为 false 的规则,这十七条构成一套不相容性演算:把结论的否定断言到前提中,在一个其相容性已由第一次运行确立的前提上重新运行同样的七十八条规则,并把由此得到的不相容读作证明。按 OWL 2 自身的定义,一个 owl:AllDifferent 集合是其 n(n−1)/2 个两两不等式的合取,因此它降为同样的形态,并且恰好在每一对都被驳倒时才被蕴涵——这就是为什么有两个条目随之离开了 schema-conclusion 类。
    • 冻结后 chase。 p rdf:type owl:TransitiveProperty 是一个全称量化的 Horn 蕴含式的缩写,而蕴含式通过对常量的概括来判定:在前提未提及的常量上冻结其规则体,重新运行规则表,并查找规则头。chain2trans1 的规则头经由 prp-spo2(78 条之一)得出。该公理的另一个合取项——p 是对象属性——是在前提自身的推理闭包中的一次查找,而且这一步不可省略:模式公理是一个合取式,只确立其中有意思的那一半,就会声称该语义并不许可的结论。
    • 概括(comprehension)。 结论可以断言某个「类存在」——一个匿名的 owl:unionOf、一个匿名的 owl:Restriction——这由基于 RDF 的语义自身的概括条件所许可,但须满足一个关于运算对象的类型附加条件。只生成结论所点名的那些脚手架,且所用的空节点已检查在两份文档中都不存在。
    • 自反性。 owl:ReflexiveProperty 在 RL 语法之外,因此该 profile 没有为它给出规则——而如果有这样一条规则,它的取值范围将是每一个资源,从而扩大每个使用方默认都会计算的推理闭包。结论自身的自环改为从前提的自反类型声明中读出。
    • 数据类型包含。 一个属性所声明的各个 rdfs:range 数据类型会取交集,而该交集可能包含于前提从未提及的某个数据类型——xsd:byte ⊑ xsd:short,以及 short ⊓ unsignedInt ⊑ unsignedShort,这两者都无法通过对三元组做连接来发现。在 XSD 值空间上判定,采用三值逻辑,否定答案只有在反例范围被精确判定时才会给出。 最后一个用例根本不需要任何判定手段,只需要其前提所点名的那份文档:webont-imports-011 通过 owl:imports 导入了一个上游清单未内联的支持本体,因此它从 W3C 自己的 URL 获取后随库固化在这些用例旁边,并作为调用方持有的配置提供给 entails()。该库仍然不获取任何内容。

    清单本身没有任何变动:rules(Regime::OwlRl) 与 implemented(Regime::OwlRl) 仍然恰好是同样的 78 条,extensions(Regime::OwlRl) 仍然只有那一条 ext-eq-diff-sym,严格的 Materialization::OwlRl 输出也与原来逐字节相同。变动的是证据——每种判定手段都带有自己的 EntailmentWarrant 分支,携带它实际使用的内容(触发的那条以 false 为结论的规则,以及一个能蕴涵该结论的最小前提子集;被冻结的常量、规则体与规则头;生成的三元组以及许可它们的推理闭包三元组),以及它自己的检查器,无需运行推理机即可重新判定全部内容。

    过去唯一一个需要采取行动(actionable)的用例由一个扩展关闭,而这个扩展是被标注出来的,而不是被吸收进去的。a owl:differentFrom b 蕴涵 b owl:differentFrom a,这是可靠的——owl:differentFrom 表示不等,而不等是对称的——其形态与 prp-symp 完全相同,却不在那 78 条规则之中,因为表 4 中关于 owl:differentFrom 的规则只会得出 false。PurRDF 把它表述为 ext-eq-diff-sym,置于一个被声明为位于每张规范表格_之外_的规则族中:extensions(Regime::OwlRl) 返回它,rules() 与 implemented() 仍然恰好是同样的 78 条且都不返回它,RuleId::is_extension 决定哪条属于哪类,而每份输出的报告都在其 missing 行旁边带有一行 extension ext-eq-diff-sym。因此调用方得到的推理闭包是表 4–9 再加上一份它可以阅读并拒绝的清单,而 OWL-RL 78 / 78 仍然只是关于表 4–9 的声明,别无其他。

实时记分板见 docs/CONFORMANCE.md。