# SHACL2FOL: An FOL Toolkit for SHACL Decision Problems

arXiv: https://arxiv.org/abs/2406.08018 · HTML: https://mlsanity.com/paper/2406.08018/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 13 references that are in the map.
- First posted on arXiv 12 Jun 2024.

## Builds on (most cited first, 4 of 4)

- [Deciding SHACL Shape Containment through Description Logics Reasoning (Extended Version)](https://mlsanity.com/paper/2008.13603/) (2020)
- [A Review of SHACL: From Data Validation to Schema Reasoning for RDF Graphs](https://mlsanity.com/paper/2112.01441/) (2021)
- [SHACL Constraints with Inference Rules](https://mlsanity.com/paper/1911.00598/) (2019)
- [Static Analysis of Graph Database Transformations](https://mlsanity.com/paper/2304.05070/) (2023)

## Built on by (most cited first, 2 of 2)

- [SHACL Validation under Graph Updates (Extended Paper)](https://mlsanity.com/paper/2508.00137/) (2025)
- [NL2SHACL-Bench: A Benchmark Suite for Natural Language to SHACL Translation](https://mlsanity.com/paper/2608.07530/) (2026)

## Abstract (arXiv)

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.