SHACL2FOL: An FOL Toolkit for SHACL Decision Problems
Paolo Pareti
TL;DR
This work tackles formal SHACL analysis by translating SHACL shape graphs into $SCL$, a fragment of $FOL$, enabling decision procedures for satisfiability, containment, and validation. It introduces SHACL2FOL, an automatic translator that outputs $TPTP$-formatted first-order theories and leverages theorem provers such as $E$ and $Vampire$ to compute answers for the static analysis problems, while also handling data-graph validation through a conjunction with $ au^{+}(G)$ and $ au^{-}(G)$. A key contribution is the $ au$ mapping from SHACL to $SCL$, along with practical UNA encoding strategies (pairwise inequality or $distinct$-typed) to scale to larger graphs, and a reduction for containment via $ au(A) \,\land\\;\neg\tau(B)$. By bridging SHACL semantics with established first-order logic and available provers, the tool lays groundwork for both theoretical exploration and practical SHACL management, with future work aimed at fuller constraint support and integration with validators and ontologies.
Abstract
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.