We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed 'g-sequents,' which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of 'inference rule types' as sets of operations that act over such objects, and define 'abstract (sequent) calculi' as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any sequent-style proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top elements in lattices correspond to nested sequent systems, while bottom elements correspond to labeled sequent systems, and observe that top and bottom elements coincide with many known (cut-free) nested and labeled sequent systems for logics characterized by Horn properties.


翻译:我们介绍了一种新颖的、与逻辑无关的证明系统研究框架,该框架涵盖了许多出现在文献中的证明理论形式和具体证明系统。特别地,我们引入了一种称为“g-sequents”的广义连词形式,它们被认为是基于Gentzen风格的连续旁证明的二元图形式。我们然后定义了各种“推断规则类型”作为在这些对象上操作的集合,并将“抽象(序言)演算”定义为由一组g-连词和有限的操作组成的对。我们的方法允许在一般情况下分析特定推断规则类型之间的相互作用,展示了在什么条件下特定类型的规则可以与其他规则交换或模拟,并适用于符合我们框架的任何连续侧证明系统。我们然后利用我们的排列和模拟结果来建立通用的演算法和证明变换算法,这些算法表明每个抽象演算法都可以有效地转化为多项式等价的抽象演算法格。我们确定了计算这个格的复杂度,并计算在格的不同演算法中证明和连词的相对大小。我们认识到格的顶部元素对应于嵌套的序言系统,而底部元素对应于标记的序言系统,并观察到顶部和底部元素与许多由Horn属性特征化的逻辑所知的(无剪切)嵌套和标记序言系统重合。

0
下载
关闭预览

相关内容

在数学和计算机科学之中,算法(Algorithm)为一个计算的具体步骤,常用于计算、数据处理和自动推理。精确而言,算法是一个表示为有限长列表的有效方法。算法应包含清晰定义的指令用于计算函数。 来自维基百科: 算法
专知会员服务
50+阅读 · 2020年12月14日
【经典书】贝叶斯编程,378页pdf,Bayesian Programming
专知会员服务
247+阅读 · 2020年5月18日
专知会员服务
159+阅读 · 2020年1月16日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
腊月廿八 | 强化学习-TRPO和PPO背后的数学
AI研习社
17+阅读 · 2019年2月2日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】SVM实例教程
机器学习研究会
17+阅读 · 2017年8月26日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
2+阅读 · 2009年12月31日
国家自然科学基金
1+阅读 · 2008年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年5月30日
Arxiv
0+阅读 · 2023年5月26日
Arxiv
0+阅读 · 2023年5月26日
VIP会员
相关资讯
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
腊月廿八 | 强化学习-TRPO和PPO背后的数学
AI研习社
17+阅读 · 2019年2月2日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】SVM实例教程
机器学习研究会
17+阅读 · 2017年8月26日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
2+阅读 · 2009年12月31日
国家自然科学基金
1+阅读 · 2008年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员