Herbrand Proofs and Expansion Proofs as Decomposed Proofs
Herbrand Proofs and Expansion Proofs as Decomposed Proofs
复制标题
Herbrand 证明和扩展证明作为分解证明
DOI：
10.1093/logcom/exaa052
复制
发表时间：
2020
影响因子：
0.7
通讯作者：
Ralph B
中科院分区：
文献类型：
--
作者：
Ralph B
通过赫布兰德定理将不可判定的一阶逻辑还原为可判定的命题逻辑长期以来一直是理论计算机科学的兴趣，赫布兰德证明的概念激发了扩展证明的定义。在本文中，我们为一阶逻辑构建了简单的深度推理系统，无论有没有剪切，这样“分解”的证明（证明的收缩和非收缩行为分离的证明）在每个系统中对应于扩展证明或 Herbrand 证明。给出了该系统中的证明、扩展证明和 Herbrand 证明之间的翻译，保留了每个方向的大部分结构。
The reduction of undecidable first-order logic to decidable propositional logic via Herbrand’s theorem has long been of interest to theoretical computer science, with the notion of a Herbrand proof motivating the definition of expansion proofs. In this paper we construct simple deep inference systems for first-order logic, both with and without cut, such that ‘decomposed’ proofs—proofs where the contractive and non-contractive behaviour of the proof is separated—in each system correspond to either expansion proofs or Herbrand proofs. Translations between proofs in this system, expansion proofs and Herbrand proofs are given, retaining much of the structure in each direction.
登录
查看更多内容
赫布兰德定理的下界
影响因子：
1.3
作者：
R. Statman
通讯作者：
R. Statman
赫布兰德定理的自然证明系统
DOI：
10.1007/978-3-319-72056-2_18
发表时间：
2018
期刊：
arXiv: Logic
影响因子：
--
作者：
B. Ralph
通讯作者：
B. Ralph
相互作用和结构的系统
DOI：
--
发表时间：
1999
期刊：
TOCL
影响因子：
--
作者：
Alessio Guglielmi
通讯作者：
Alessio Guglielmi
DOI：
--
发表时间：
1987
期刊：
Studia Logica: An International Journal for Symbolic Logic
影响因子：
--
作者：
D. Miller
通讯作者：
D. Miller
DOI：
10.1007/3-540-60178-3_85
发表时间：
1994-10
期刊：
--
影响因子：
--
作者：
S. Buss
通讯作者：
S. Buss