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.

翻译：近期关于形状约束语言（SHACL）——一种用于验证RDF图的W3C规范——的研究依赖于将该语言翻译为一阶逻辑，从而为验证、包含性和可满足性决策问题提供形式化解决方案。延续这一研究方向，我们推出了SHACL2FOL，这是首个能够（i）将SHACL文档转换为一阶逻辑语句，并（ii）计算可满足性和包含性这两类静态分析问题答案的自动化工具；该工具还允许测试图相对于一组约束的有效性。通过与E和Vampire等现有定理证明器集成，该工具可计算上述决策问题的答案，并以标准TPTP格式输出对应的一阶逻辑理论。我们相信，该工具通过提供其语义的自动一阶逻辑解释，可助力SHACL的进一步理论研究，同时通过提供静态分析能力以辅助SHACL约束的创建与管理，使SHACL实践者受益。