Synthesizing Nested Relational Queries from Implicit Specifications
Synthesizing Nested Relational Queries from Implicit Specifications
复制标题
从隐式规范合成嵌套关系查询
DOI：
10.1145/3584372.3588653
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Benedikt M
中科院分区：
文献类型：
--
作者：
Benedikt M
派生数据集可以隐式或显式定义。隐式定义（数据集O的数据集I）是涉及源数据I和接口数据O的逻辑规范。如果规范的任何两个模型都同意我同意O，那么就I而言，它是O的有效定义。相反，显式定义是从I产生O的查询。Beth定理的变体说明可以将隐式定义转换为显式定义。此外，在适当的证明系统中，如果证明证明具有隐式可定义性，则可以有效地实现这种转换。我们证明了嵌套关系的类似的隐式到显式的有效结果：嵌套关系的自然逻辑中给出的隐式定义可以有效地转换为嵌套关系演算（NRC）中的显式定义。因此，我们可以根据NRC视图有效地提取NRC查询的重写，只要证明查询是由视图决定的。
Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving the source data I and the interface data O. It is a valid definition of O in terms of I, if any two models of the specification agreeing on I agree on O. In contrast, an explicit definition is a query that produces O from I. Variants of Beth's theorem state that one can convert implicit definitions to explicit ones. Further, this conversion can be done effectively given a proof witnessing implicit definability in a suitable proof system. We prove the analogous effective implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be effectively converted to explicit definitions in the nested relational calculus (NRC). As a consequence, we can effectively extract rewritings of NRC queries in terms of NRC views, given a proof witnessing that the query is determined by the views.
登录
查看更多内容
数理逻辑年鉴
DOI：
--
发表时间：
1969
期刊：
Journal of Symbolic Logic (JSL)
影响因子：
--
作者：
ScienceDirect
通讯作者：
ScienceDirect
受保护逻辑中的有效插值和保存
DOI：
10.1145/2603088.2603108
发表时间：
2014
期刊：
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
影响因子：
--
作者：
Michael Benedikt;B. T. Cate;M. V. Boom
通讯作者：
M. V. Boom
Beth 受保护片段的可定义性
DOI：
--
发表时间：
1999
期刊：
Logic Programming and Automated Reasoning
影响因子：
--
作者：
E. Hoogland;maarten marx;M. Otto
通讯作者：
M. Otto
DOI：
10.1016/s0049-237x(09)70162-4
发表时间：
1985
期刊：
Studies in logic and the foundations of mathematics
影响因子：
--
作者：
A. Scedrov
通讯作者：
A. Scedrov
结构证明理论
DOI：
10.1017/cbo9780511527340
发表时间：
2001
期刊：
ACM Transactions on Computational Logic (TOCL)
影响因子：
--
作者：
Sara Negri;J. Plato
通讯作者：
J. Plato