Cut Elimination inside a Deep Inference System for Classical Predicate Logic
Cut Elimination inside a Deep Inference System for Classical Predicate Logic
复制标题
经典谓词逻辑的深度推理系统中的剪切消除
DOI：
10.1007/s11225-006-6605-4
复制
发表时间：
2006
期刊：
影响因子：
0.7
通讯作者：
Kai Brünnler
中科院分区：
文献类型：
--
作者：
Kai Brünnler
深度推理是单边递归演算的自然推广，其中规则被允许深入应用于公式内部，就像在项重写中重写规则一样。这种应用推理规则的自由度允许表达在无割演算中难以或不可能表达的逻辑系统，并且它还允许比无割演算更细粒度的推导分析。然而，同样的自由度也使得进行这种分析变得更加困难，特别是设计切割消除程序变得更加困难。在本文中，我们看到一个削减消除过程的深推理系统的经典谓词逻辑。因此，我们得出Herbrand定理，我们表示为一个因式分解的衍生物。
Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations.