关于切割与收缩的置换
逻辑
2007-05-23 v1
摘要
本文给出直觉主义命题逻辑的一种消去切割过程，其中切割被直接消去，而不引入多重切割规则 mix，并且将切割推向收缩之上是一项归约步骤。在给出此过程之前，从切割与收缩置换的视角对 Gentzen 的 mix-消去过程作了分析。还表明在缺乏蕴涵的情况下，将切割推向收缩之上对于直接消去切割并不构成问题。
引用
@article{arxiv.math/9911065,
title = {On Permuting Cut with Contraction},
author = {Mirjana Borisavljevic and Kosta Dosen and Zoran Petric},
journal= {arXiv preprint arXiv:math/9911065},
year = {2007}
}
备注
32 pages, to appear in Mathematical Structures in Computer Science