Soundness and Completeness of SPARQL Query Containment Solver SpeCS

TL;DR

This paper proves the correctness of the SPECS tool for reasoning about SPARQL query containment, establishing its soundness and completeness for various query types, thereby advancing automated query analysis.

Contribution

It provides formal proofs of soundness and completeness for SPECS's approach to SPARQL query containment, including non-conjunctive queries with operators like union and optional.

Findings

Proves correctness of SPECS for conjunctive queries

Establishes soundness and completeness for certain non-conjunctive queries

Formalizes semantics of a core subset of SPARQL

Abstract

Tool SPECS implements an efficient automated approach for reasoning about the SPARQL query containment problem. In this paper, we prove the correctness of this approach. We give precise semantics of the core subset of SPARQL language. We briefly discuss the procedure used for reducing the query containment problem into a formal logical framework. We prove that such reduction is both sound and complete for conjunctive queries, and also for some important cases of non-conjunctive queries containing operator union, operator optional, and subqueries. Soundness and completeness proofs are considered in both containment and subsumption forms.