Pith. sign in

REVIEW

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2210.07083 v1 pith:7JJ364FJ submitted 2022-10-13 cs.LO cs.DB

Soundness and Completeness of SPARQL Query Containment Solver SpeCS

Mirko Spasi\'c , Milena Vujo\v{s}evi\'c Jani\v{c}i\'c This is my paper
classification cs.LO cs.DB
keywords containmentquerysparqlapproachcompletenessoperatorproblemprove
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.