Static Analysis of Recursive SHACL

• URL: http://arxiv.org/abs/2605.02787v1
• Date: Mon, 04 May 2026 16:29:29 GMT
• Title: Static Analysis of Recursive SHACL
• Abstract summary: SHACL (Shapes Constraint Language) expresses constraints on RDF data by means of so-called shapes.<n>Our key technical contribution is a translation of SHACL under the well-founded semantics into the full hybrid mu-calculus.
• Score: 5.161531917413707
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: SHACL (Shapes Constraint Language) expresses constraints on RDF data by means of so-called shapes. Its central service is validation: verifying whether a data graph complies with a SHACL document. But so far, there are no static analysis services to compare documents. In this paper, we study the following problem: decide whether all graphs that validate one SHACL document also validate another. Unlike previous works that have considered the implication of shape expressions only, we consider documents comprising (recursive) shape definitions and targets. We show that implication (a.k.a. containment) is undecidable under the supported and the stable model semantics, even for the fragment that uses the description logic ALCIO for shape expressions. Under the well-founded semantics, in surprising contrast, it is decidable in single exponential time. Our key technical contribution is a translation of SHACL under the well-founded semantics into the full hybrid mu-calculus, revealing a novel link between well-founded models and a fixed point modal logic, and a worst-case optimal automata-based decision procedure.

Related papers

• The Illusion of High Utility in Safety Alignment of Text-to-Image Diffusion Models [49.67749928542536]
  Safety alignment of text-to-image (T2I) diffusion models aims to suppress harmful generations while preserving utility on benign prompts.<n>Recent methods often appear to deliver high safety with high utility, but this conclusion rests largely on coarse global utility metrics.<n>We show that when utility is measured with structured evaluation, this illusion breaks: onA (Text-to-Image Faithfulness evaluation with Question Answering)<n>We propose StructureAware Geometric Regularization (SAGE), a safety alignment objective that explicitly preserves embedding spread and inter-prompt relational structure.
  arXiv  Detail & Related papers  (2026-07-01T04:00:27Z)
• Finite Certificates for In-Context Determinacy and a Threshold Theory of Emergence in Language Models [0.2864713389096699]
  This paper develops a model-theoretic framework for verifying context-conditioned language-model behavior.<n>It provides finite context certificates, pair-separator hitting sets, query teaching dimension, prompt-preservation criteria, and scale-limit witnesses.
  arXiv  Detail & Related papers  (2026-05-30T14:07:58Z)
• Geometrically-Constrained Agent for Spatial Reasoning [53.93718394870856]
  Vision Language Models exhibit a fundamental semantic-to-geometric gap in spatial reasoning.<n>Current paradigms fail to bridge this gap.<n>We propose a training-free agentic paradigm that resolves this gap by introducing a formal task constraint.
  arXiv  Detail & Related papers  (2025-11-27T17:50:37Z)
• SHACL Validation under Graph Updates (Extended Paper) [6.755812289103844]
  We present a SHACL-based update language that can capture intuitive and realistic modifications on RDF graphs.<n>This problem asks to verify whether every graph that validates a SHACL specification will still do so after applying a given update sequence.<n>We show that static validation can be reduced to (un)satisfiability of constraints in (a minor extension) SHACL.
  arXiv  Detail & Related papers  (2025-07-31T19:58:16Z)
• SHACL Validation in the Presence of Ontologies: Semantics and Rewriting Techniques [6.882042556551609]
  SHACL is a constraint language that treats the data as complete and must be validated under the closed-world assumption.<n>We advocate a semantics for SHACL validation in the presence of major core universal models.<n>We show that even very simple features make the problem EXPTIME-complete, and PTIME-complete in data complexity.
  arXiv  Detail & Related papers  (2025-07-16T14:38:27Z)
• SHACL2FOL: An FOL Toolkit for SHACL Decision Problems [0.4895118383237099]
  We introduce SHACL2FOL, the first automatic tool that translates SHACL documents into FOL sentences. The tool 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.
  arXiv  Detail & Related papers  (2024-06-12T09:20:25Z)
• Telling Left from Right: Identifying Geometry-Aware Semantic Correspondence [80.6840060272386]
  This paper identifies the importance of being geometry-aware for semantic correspondence. We show that incorporating this information can markedly enhance semantic correspondence performance. Our method achieves a PCK@0.10 score of 65.4 (zero-shot) and 85.6 (supervised) on the challenging SPair-71k dataset.
  arXiv  Detail & Related papers  (2023-11-28T18:45:13Z)
• Interpretable Automatic Fine-grained Inconsistency Detection in Text Summarization [56.94741578760294]
  We propose the task of fine-grained inconsistency detection, the goal of which is to predict the fine-grained types of factual errors in a summary. Motivated by how humans inspect factual inconsistency in summaries, we propose an interpretable fine-grained inconsistency detection model, FineGrainFact.
  arXiv  Detail & Related papers  (2023-05-23T22:11:47Z)
• FactGraph: Evaluating Factuality in Summarization with Semantic Graph Representations [114.94628499698096]
  We propose FactGraph, a method that decomposes the document and the summary into structured meaning representations (MRs) MRs describe core semantic concepts and their relations, aggregating the main content in both document and summary in a canonical form, and reducing data sparsity. Experiments on different benchmarks for evaluating factuality show that FactGraph outperforms previous approaches by up to 15%.
  arXiv  Detail & Related papers  (2022-04-13T16:45:33Z)
• Satisfiability and Containment of Recursive SHACL [4.8986598953553555]
  The Shapes Constraint Language (SHACL) is the recent W3C recommendation language for validating RDF data, by verifying certain shapes on graphs. Previous work has largely focused on the validation problem and the standard decision problems of satisfiability and containment. We provide a comprehensive study of the different features of SHACL, by providing a translation to a new first-order language, called SCL, that precisely captures the semantics of SHACL. We also present MSCL, a second-order extension of SCL, which allows us to define, in a single formal logic framework, the main
  arXiv  Detail & Related papers  (2021-08-30T08:51:03Z)
• Leveraging Unlabeled Data for Entity-Relation Extraction through Probabilistic Constraint Satisfaction [54.06292969184476]
  We study the problem of entity-relation extraction in the presence of symbolic domain knowledge. Our approach employs semantic loss which captures the precise meaning of a logical sentence. With a focus on low-data regimes, we show that semantic loss outperforms the baselines by a wide margin.
  arXiv  Detail & Related papers  (2021-03-20T00:16:29Z)
• SHACL Satisfiability and Containment (Extended Paper) [6.308539010172308]
  The Shapes Constraint Language (SHACL) is a recent W3C recommendation language for validating RDF data. In this paper, we undertake a thorough study of different features of non-recursive SHACL by providing a translation to a new first-order language, called SCL. We study the interaction of SHACL features in this logic and provide the detailed map of decidability and complexity results of the aforementioned decision problems for different SHACL sublanguages.
  arXiv  Detail & Related papers  (2020-08-31T14:52:03Z)
• Grounded and Controllable Image Completion by Incorporating Lexical Semantics [111.47374576372813]
  Lexical Semantic Image Completion (LSIC) may have potential applications in art, design, and heritage conservation. We advocate generating results faithful to both visual and lexical semantic context. One major challenge for LSIC comes from modeling and aligning the structure of visual-semantic context.
  arXiv  Detail & Related papers  (2020-02-29T16:54:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.