The Circularity Principle was successfully applied for developing a coinductive proving technique, known as circular coinduction. In this paper, we show that the same principle can be used to develop an inductive proving technique. A main advantage of this uniform approach is that the two proving techniques can be easily combined during the verification process. Circular induction is simple, flexible, generic, and therefore it is a good candidate framework for combining different proving schemes into a competitive tool. We exhibit this potential by presenting how the circular induction is implemented in CIRC, a prover built around the Circularity Principle. Disclaimer. This paper was written in 2010, at the time the CIRC prover was developed, and the main body reflects the state of the work and of the prover as of that date. For this arXiv technical report, only the related-work discussion (Section 6) and the concluding section have been revised: Section 6 has been extended to situate circular induction within the cyclic-proof and infinite-descent literature that has appeared or matured since 2010. No other part of the paper-its definitions, results, proofs, examples, or implementation description-has been modified, and the technical content should be read as a 2010 contribution. References to developments after 2010 appear only in the updated related-work section.


翻译:循环性原则已成功应用于开发一种余归纳证明技术,即循环余归纳。本文表明,相同原则也可用于开发归纳证明技术。这种统一方法的主要优势在于,在验证过程中可以轻松组合这两种证明技术。循环归纳简单、灵活且通用,因此是结合不同证明方案形成竞争性工具的优良框架。我们通过展示循环归纳如何在CIRC(一个基于循环性原则构建的证明器)中实现来体现这一潜力。免责声明:本文写于2010年,即CIRC证明器开发之时,主体内容反映了当时的工作和证明器状态。为本次arXiv技术报告,仅修订了相关工作讨论(第6节)和结论部分:第6节已扩展,将循环归纳置于2010年以来出现或成熟的循环证明与无限下降文献中。论文其他部分——其定义、结果、证明、示例或实现描述——均未修改,技术内容应视为2010年的贡献。2010年后的发展参考文献仅出现在更新的相关工作部分。

0
下载
关闭预览

相关内容

【NTU博士论文】当深度学习遇上归纳逻辑程序设计
专知会员服务
24+阅读 · 2025年5月6日
《序列推荐》最新综述
专知会员服务
22+阅读 · 2024年12月27日
万字综述,GNN在NLP中的应用,建议收藏慢慢看
专知会员服务
59+阅读 · 2021年6月22日
因果关联学习,Causal Relational Learning
专知会员服务
185+阅读 · 2020年4月21日
【AAAI2021】对比聚类,Contrastive Clustering
专知
26+阅读 · 2021年1月30日
图节点嵌入(Node Embeddings)概述,9页pdf
专知
15+阅读 · 2020年8月22日
推荐系统原理、工程、大厂(Youtube、BAT、TMB)架构干活分享
开年重磅——周志华团队综述归纳逻辑程序设计
计算机研究与发展
10+阅读 · 2019年1月22日
博客 | 回归类算法最全综述及逻辑回归重点讲解
AI研习社
13+阅读 · 2018年11月29日
线性回归:简单线性回归详解
专知
12+阅读 · 2018年3月10日
图上的归纳表示学习
科技创新与创业
23+阅读 · 2017年11月9日
国家自然科学基金
6+阅读 · 2017年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
9+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
23+阅读 · 2008年12月31日
Arxiv
0+阅读 · 6月9日
Arxiv
0+阅读 · 5月20日
Arxiv
0+阅读 · 5月8日
Arxiv
0+阅读 · 5月5日
VIP会员
最新内容
学习数据的几何:形状空间分析数学综述
专知会员服务
2+阅读 · 6月17日
定向能反无人机系统最新发展动态
专知会员服务
6+阅读 · 6月17日
从燃煤战舰到算法战争:水面指挥的永恒要求
专知会员服务
3+阅读 · 6月17日
相关资讯
【AAAI2021】对比聚类,Contrastive Clustering
专知
26+阅读 · 2021年1月30日
图节点嵌入(Node Embeddings)概述,9页pdf
专知
15+阅读 · 2020年8月22日
推荐系统原理、工程、大厂(Youtube、BAT、TMB)架构干活分享
开年重磅——周志华团队综述归纳逻辑程序设计
计算机研究与发展
10+阅读 · 2019年1月22日
博客 | 回归类算法最全综述及逻辑回归重点讲解
AI研习社
13+阅读 · 2018年11月29日
线性回归:简单线性回归详解
专知
12+阅读 · 2018年3月10日
图上的归纳表示学习
科技创新与创业
23+阅读 · 2017年11月9日
相关基金
国家自然科学基金
6+阅读 · 2017年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
9+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
23+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员