一句话：证明布尔逻辑中仅含线性推理的重写系统其非平凡推导长度多项式有界，并推出不存在多项式时间可判定的完备线性推理系统，除非 coNP=NP。
近年来线性规则在结构证明论中日益重要：布尔逻辑中所有可靠的线性推理规则集合已是 coNP 完全的，每个布尔重言式都可写为左右线性重写规则。本文研究仅由线性推理构成的系统，证明其中任何“非平凡”推导的长度都受多项式界定；由此得到，除非 coNP=NP，否则不存在多项式时间可判定且可靠完备的线性推理系统。方法上借用项重写、布尔函数论与图论的工具，并在这些领域间建立联系，为布尔逻辑的线性项重写系统提供统一理论框架。
Linear rules have played an increasing role in structural proof theory in recent years. It has been observed that the set of all sound linear inference rules in Boolean logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-)linear rewrite rule. In this paper we study properties of systems consisting only of linear inferences. Our main result is that the length of any 'nontrivial' derivation in such a system is bound by a polynomial. As a consequence there is no polynomial-time decidable sound and complete system of linear inferences, unless coNP=NP. We draw tools and concepts from term rewriting, Boolean function theory and graph theory in order to access some required intermediate results. At the same time we make several connections between these areas that, to our knowledge, have not yet been presented and constitute a rich theoretical framework for reasoning about linear TRSs for Boolean logic.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{DasS16,
title = {On linear rewriting systems for Boolean logic and some applications to proof theory},
author = {Anupam Das and Lutz Straßburger},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 4},
year = {2017},
doi = {10.2168/lmcs-12(4:9)2016}
}