Proof Transformations and Structural Invariance
Proof Transformations and Structural Invariance
复制标题
证明变换和结构不变性
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
A. Leitsch
中科院分区：
文献类型：
--
作者：
Stefan Hetzl;A. Leitsch
在本文中，我们定义了一个配置文件的概念，这是一个特征子句集，对应于一阶逻辑中的一个LK-证明，这是不变的规则排列。它示出（通过cutelimination），该配置文件甚至是不变的一大类证明变换（称为“简单变换”），其中包括变换否定范式。作为证据具有相同的配置文件显示相同的行为w.r.t.割消（可以通过CERES方法正式定义），通过简单变换获得的证明在这个意义上可以被认为是相等的。与相关结果的基础上的证明网的比较：特别是它表明，具有相同的配置文件的证明定义一个更大的等价类比那些具有相同的证明网。
In this paper we define the concept of a profile, which is a characteristic clause set, corresponding to an LK-proof in first-order logic, which is invariant under rule permutations. It is shown (via cutelimination) that the profile is even invariant under a large class of proof transformations (called "simple transformations"), which includes transformations to negation normal form. As proofs having the same profile show the same behavior w.r.t. cut-elimination (which can be formally defined via the method CERES), proofs obtained by simple transformations can be considered as equal in this sense. A comparison with related results based on proof nets is given: in particular it is shown that proofs having the same profile define a larger equivalence class than those having the same proof net.