We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formulas -- the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.


翻译:我们提出了一个新颖的逻辑,称为框架逻辑(FL),它利用一个构思 Sp (.) 来扩展第一阶逻辑(带有递归定义),它能捕捉公式的隐含支持 -- -- 其含义所依赖的宇宙的精密子集。我们利用这种支持,制定证据规则,在基本模型发生变化时,为框架推理提供优雅的便利。我们通过捕捉若干数据结构来显示逻辑的表达方式,并展示从精确的分离逻辑碎片到逻辑框架的翻译。最后,我们设计了一个程序逻辑,根据框架逻辑进行推理,其程序能动态地更新堆积,便于本地的规格和框架推理。这个程序逻辑包括本地化的证明规则以及从FL中得出最薄弱的最严格先决条件的规则。

0
下载
关闭预览

相关内容

专知会员服务
123+阅读 · 2020年9月8日
专知会员服务
38+阅读 · 2020年9月6日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
IEEE ICKG 2022: Call for Papers
机器学习与推荐算法
3+阅读 · 2022年3月30日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
ACM TOMM Call for Papers
CCF多媒体专委会
2+阅读 · 2022年3月23日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
【ICIG2021】Latest News & Announcements of the Workshop
中国图象图形学学会CSIG
0+阅读 · 2021年12月20日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium9
中国图象图形学学会CSIG
0+阅读 · 2021年12月17日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium3
中国图象图形学学会CSIG
0+阅读 · 2021年11月9日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Arxiv
0+阅读 · 2022年11月1日
Arxiv
0+阅读 · 2022年10月30日
Arxiv
0+阅读 · 2022年10月28日
VIP会员
相关VIP内容
专知会员服务
123+阅读 · 2020年9月8日
专知会员服务
38+阅读 · 2020年9月6日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
IEEE ICKG 2022: Call for Papers
机器学习与推荐算法
3+阅读 · 2022年3月30日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
ACM TOMM Call for Papers
CCF多媒体专委会
2+阅读 · 2022年3月23日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
【ICIG2021】Latest News & Announcements of the Workshop
中国图象图形学学会CSIG
0+阅读 · 2021年12月20日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium9
中国图象图形学学会CSIG
0+阅读 · 2021年12月17日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium3
中国图象图形学学会CSIG
0+阅读 · 2021年11月9日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Top
微信扫码咨询专知VIP会员