论文标题
部分可观测时空混沌系统的无模型预测
Soundness and Completeness of SPARQL Query Containment Solver 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.
