Structural proof theory is praised for being a symbolic approach to reasoning and proofs, in which one can define schemas for reasoning steps and manipulate proofs as a mathematical structure. For this to be possible, proof systems must be designed as a set of rules such that proofs using those rules are correct by construction. Therefore, one must consider all ways these rules can interact and prove that they satisfy certain properties which makes them "well-behaved". This is called the meta-theory of a proof system. Meta-theory proofs typically involve many cases on structures with lots of symbols. The majority of cases are usually quite similar, and when a proof fails, it might be because of a sub-case on a very specific configuration of rules. Developing these proofs by hand is tedious and error-prone, and their combinatorial nature suggests they could be automated. There are various approaches on how to automate, either partially or completely, meta-theory proofs. In this paper, I will present some techniques that I have been involved in for facilitating meta-theory reasoning.


翻译:结构性证据理论被称赞为一种对推理和证据的象征性方法,在这种方法中,人们可以界定推理步骤的模型,并将证据作为数学结构来操纵证据。要做到这一点,就必须将证据系统设计成一套规则,使使用这些规则的证明能够通过构建来正确。因此,我们必须考虑所有这些规则能够相互作用并证明它们满足某些特性,从而使其“以良好方式执行”的各种方式。这被称为一个证明系统的元理论。元理论证据通常涉及许多带有许多符号的结构上的许多案例。多数案例通常非常相似,当证据失败时,这可能是由于规则的非常具体配置的子案例。用手来开发这些证据是乏味和易出错的,其组合性质表明它们可以自动化。对于如何将部分或完全的元理论证据自动化,有多种方法。在本文中,我将介绍一些我参与其中的技巧,以促进元理论推理。

0
下载
关闭预览

相关内容

CASES:International Conference on Compilers, Architectures, and Synthesis for Embedded Systems。 Explanation:嵌入式系统编译器、体系结构和综合国际会议。 Publisher:ACM。 SIT: http://dblp.uni-trier.de/db/conf/cases/index.html
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
机器学习在材料科学中的应用综述,21页pdf
专知会员服务
48+阅读 · 2019年9月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【论文】图上的表示学习综述
机器学习研究会
14+阅读 · 2017年9月24日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
12+阅读 · 2021年5月3日
Arxiv
3+阅读 · 2020年11月26日
Neural Module Networks for Reasoning over Text
Arxiv
9+阅读 · 2019年12月10日
Arxiv
15+阅读 · 2018年4月5日
Arxiv
6+阅读 · 2018年1月29日
VIP会员
相关VIP内容
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
机器学习在材料科学中的应用综述,21页pdf
专知会员服务
48+阅读 · 2019年9月24日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【论文】图上的表示学习综述
机器学习研究会
14+阅读 · 2017年9月24日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
相关论文
Top
微信扫码咨询专知VIP会员