SHACL2FOL: An FOL Toolkit for SHACL Decision Problems
This tool aids SHACL practitioners by providing static analysis capabilities for constraint management, but it is incremental as it builds on prior translation-based research.
The authors tackled the problem of validating RDF graphs using SHACL by developing SHACL2FOL, an automatic tool that translates SHACL documents into first-order logic and computes answers to satisfiability, containment, and validation decision problems, integrating with existing theorem provers like E and Vampire.
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.