A Local System for Classical Logic
A Local System for Classical Logic
复制标题
经典逻辑的局部系统
DOI：
10.1007/3-540-45653-8_24
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Alwen Tiu
中科院分区：
文献类型：
--
作者：
Kai Brünnler;Alwen Tiu
结构演算是一种用于指定逻辑系统的框架，它类似于单边结构演算，但更一般。在这个新的框架下，我们给出了命题经典逻辑的一个推理规则系统，并证明了它的割消，该系统具有一个在逻辑演算中不存在的导子分解定理.我们的系统的主要新奇在于，所有的规则都是局部的：特别是收缩，被简化为原子形式。这对于分布式证明搜索和复杂性理论来说应该是有趣的，因为应用每个规则的计算成本是有界的。
The calculus of structures is a framework for specifying logical systems, which is similar to the one-sided sequent calculus but more general. We present a system of inference rules for propositional classical logic in this new framework and prove cut elimination for it. The system enjoys a decomposition theorem for derivations that is not available in the sequent calculus. The main novelty of our system is that all the rules are local: contraction, in particular, is reduced to atomic form. This should be interesting for distributed proof-search and also for complexity theory, since the computational cost of applying each rule is bounded.