Recent studies on the Shapes Constraint Language (SHACL), a W3C specification
for validating RDF graphs, rely on translating the language into first-order
logic in order to provide formally-grounded solutions to the validation,
containment and satisfiability decision problems. Continuing on this line of
research, we introduce SHACL2FOL, the first automatic tool that (i) translates
SHACL documents into FOL sentences and (ii) computes the answer to the two
static analysis problems of satisfiability and containment; it also allow to
test the validity of a graph with respect to a set of constraints. By
integrating with existing theorem provers, such as E and Vampire, the tool
computes the answer to the aforementioned decision problems and outputs the
corresponding first-order logic theories in the standard TPTP format. We
believe this tool can contribute to further theoretical studies of SHACL, by
providing an automatic first-order logic interpretation of its semantics, while
also benefiting SHACL practitioners, by supplying static analysis capabilities
to help the creation and management of SHACL constraints.

SHACL2FOL 是一款自动工具，能将 SHACL 文档转换为 FOL 句子，并计算满足性和包含性这两个静态分析问题的答案，进而通过与 E 和 Vampire 等定理证明器集成，输出相应的一阶逻辑理论。这个工具可以提供 SHACL 语义的自动一阶逻辑解释，同时为 SHACL 约束的创建和管理提供静态分析功能，从而有助于 SHACL 的进一步理论研究和实践应用。

SHACL2FOL：SHACL 决策问题的 FOL 工具包

SHACL2FOL: An FOL Toolkit for SHACL Decision Problems

We present a formal semantics and proof of soundness for shapes schemas, an
expressive schema language for RDF graphs that is the foundation of Shape
Expressions Language 2.0. It can be used to describe the vocabulary and the
structure of an RDF graph, and to constrain the admissible properties and
values for nodes in that graph. The language defines a typing mechanism called
shapes against which nodes of the graph can be checked. It includes an
algebraic grouping operator, a choice operator and cardinality constraints for
the number of allowed occurrences of a property. Shapes can be combined using
Boolean operators, and can use possibly recursive references to other shapes.
We describe the syntax of the language and define its semantics. The
semantics is proven to be well-defined for schemas that satisfy a reasonable
syntactic restriction, namely stratified use of negation and recursion. We
present two algorithms for the validation of an RDF graph against a shapes
schema. The first algorithm is a direct implementation of the semantics,
whereas the second is a non-trivial improvement. We also briefly give
implementation guidelines.

本文介绍了一个用于描述 RDF 图的词汇和结构，并限制节点的允许属性和值的表达式语言 Shape Expressions Language 2.0 中的 shapes schemas，定义了其语法和语义，并证明了允许负数和递归调用的模式符合合理的语法限制。作者展示了两个算法用于 RDF 图的验证，并提出了一些实现指南。