SHACL2FOL: An FOL Toolkit for SHACL Decision Problems

最近关于 Shapes Constraint Language (SHACL) 的研究主要依赖于将该语言转化为一阶逻辑，以提供形式化基础的解决方案，来解决验证、包含和可满足性决策问题。在这一研究方向的基础上，我们推出了 SHACL2FOL 工具，这是第一个自动化工具，它可以 (i) 将 SHACL 文档翻译成 FOL 句子，并且 (ii) 计算可满足性和包含的两个静态分析问题的答案；它还允许测试图形是否符合一组约束条件。通过与现有的定理证明器（如 E 和 Vampire）集成，该工具计算了上述决策问题的答案，并输出标准 TPTP 格式的相应一阶逻辑理论。我们相信，这个工具可以为 SHACL 的进一步理论研究做出贡献，通过提供其语义的自动化一阶逻辑解释，同时也可以为 SHACL 的实践者提供静态分析能力，以帮助创建和管理 SHACL 约束。

论文旨在介绍SHACL2FOL工具，解决SHACL语言的验证、包含和可满足性决策问题，并为SHACL从业者提供静态分析能力，以帮助创建和管理SHACL约束。

SHACL2FOL是一种自动化工具，可将SHACL文档转换为FOL句子，并计算满足性和包含性的两个静态分析问题的答案。它与现有的定理证明器（如E和Vampire）集成，可以计算上述决策问题的答案，并以标准TPTP格式输出相应的FOL理论。

该工具为SHACL语言的语义提供了自动的一阶逻辑解释，并为SHACL从业者提供了静态分析能力。实验结果表明，SHACL2FOL能够快速而准确地解决验证、包含和可满足性决策问题。该工具还提供了开源代码。

最近的相关研究主要集中在SHACL语言的应用和扩展。例如，有论文介绍了使用SHACL来验证Linked Data的一致性，以及使用SHACL来生成数据质量报告。