We consider constrained Horn clause solving from the more general point of view of solving formula equations. Constrained Horn clauses correspond to the subclass of Horn formula equations. We state and prove a fixed-point theorem for Horn formula equations which is based on expressing the fixed-point computation of a minimal model of a set of Horn clauses on the object level as a formula in first-order logic with a least fixed point operator. We describe several corollaries of this fixed-point theorem, in particular concerning the logical foundations of program verification, and sketch how to generalise it to incorporate abstract interpretations.


翻译:我们从解决公式方程的更普遍的角度考虑限制的合恩条款的解决。受约束的合恩条款与合恩公式方程的子类相对应。我们提出并证明合恩公式方程的固定点理论。 我们提出并证明合恩公式方程的固定点理论,该方程的基础是将一组合恩条款在目标水平上的最低模式的固定点计算作为一阶逻辑中的一种公式,并且有一个最不固定点操作员。我们描述了这一固定点方程的若干轮廓,特别是关于程序核查的逻辑基础,并勾画如何将其概括为包含抽象解释。

0
下载
关闭预览

相关内容

ACM/IEEE第23届模型驱动工程语言和系统国际会议,是模型驱动软件和系统工程的首要会议系列,由ACM-SIGSOFT和IEEE-TCSE支持组织。自1998年以来,模型涵盖了建模的各个方面,从语言和方法到工具和应用程序。模特的参加者来自不同的背景,包括研究人员、学者、工程师和工业专业人士。MODELS 2019是一个论坛,参与者可以围绕建模和模型驱动的软件和系统交流前沿研究成果和创新实践经验。今年的版本将为建模社区提供进一步推进建模基础的机会,并在网络物理系统、嵌入式系统、社会技术系统、云计算、大数据、机器学习、安全、开源等新兴领域提出建模的创新应用以及可持续性。 官网链接:http://www.modelsconference.org/
专知会员服务
27+阅读 · 2021年7月3日
专知会员服务
41+阅读 · 2021年4月2日
【干货书】机器学习速查手册,135页pdf
专知会员服务
125+阅读 · 2020年11月20日
【清华大学】图随机神经网络,Graph Random Neural Networks
专知会员服务
154+阅读 · 2020年5月26日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
58+阅读 · 2019年10月17日
【深度学习视频分析/多模态学习资源大列表】
专知会员服务
91+阅读 · 2019年10月16日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【泡泡汇总】CVPR2019 SLAM Paperlist
泡泡机器人SLAM
14+阅读 · 2019年6月12日
ICLR2019最佳论文出炉
专知
12+阅读 · 2019年5月6日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
视频超分辨 Detail-revealing Deep Video Super-resolution 论文笔记
统计学习与视觉计算组
17+阅读 · 2018年3月16日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Arxiv
0+阅读 · 2021年11月1日
Pointer Graph Networks
Arxiv
7+阅读 · 2020年6月11日
VIP会员
相关主题
相关VIP内容
专知会员服务
27+阅读 · 2021年7月3日
专知会员服务
41+阅读 · 2021年4月2日
【干货书】机器学习速查手册,135页pdf
专知会员服务
125+阅读 · 2020年11月20日
【清华大学】图随机神经网络,Graph Random Neural Networks
专知会员服务
154+阅读 · 2020年5月26日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
58+阅读 · 2019年10月17日
【深度学习视频分析/多模态学习资源大列表】
专知会员服务
91+阅读 · 2019年10月16日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
相关资讯
【泡泡汇总】CVPR2019 SLAM Paperlist
泡泡机器人SLAM
14+阅读 · 2019年6月12日
ICLR2019最佳论文出炉
专知
12+阅读 · 2019年5月6日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
视频超分辨 Detail-revealing Deep Video Super-resolution 论文笔记
统计学习与视觉计算组
17+阅读 · 2018年3月16日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Top
微信扫码咨询专知VIP会员