SPARQL查询包容求解器SpeCS的可靠性和完备性
Soundness and Completeness of SPARQL Query Containment Solver SpeCS
摘要：
SPECS工具实现了一种高效的自动化方法来推理SPARQL查询包含问题。在本文中，我们证明了这种方法的正确性。给出了SPARQL语言核心子集的精确语义。我们简要地讨论了用于减少到一个正式的逻辑框架的查询包含问题的过程。我们证明，这种减少是健全的和完整的合取查询，也为一些重要的情况下，非合取查询包含操作工会，操作员可选，和子查询。可靠性和完整性证明被认为是在遏制和包容的形式。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
