SHACL2FOL: An FOL Toolkit for SHACL Decision Problems

TL;DR

SHACL2FOL is an automatic tool that translates SHACL constraints into first-order logic, enabling formal analysis of RDF graph validation, containment, and satisfiability problems using theorem provers.

Contribution

This paper introduces SHACL2FOL, the first tool to automatically translate SHACL into FOL and solve key static analysis problems, bridging practical validation and formal logic.

Findings

Successfully translates SHACL to FOL for validation tasks

Integrates with theorem provers like E and Vampire

Enables automatic analysis of SHACL constraints

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.