A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. Equivalently, it is a linear rewrite rule on Boolean terms that constitutes a valid implication. Linear inferences have played a significant role in structural proof theory, in particular in models of substructural logics and in normalisation arguments for deep inference proof systems. In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find four `minimal' 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. Two of these new inferences derive some previously found independent linear inferences. The other two (which are dual) exhibit structure seemingly beyond the scope of previous approaches we are aware of; in particular, their existence contradicts a conjecture of Das and Strassburger. We were also able to identify 10 minimal 9-variable linear inferences independent of all the aforementioned inferences, comprising 5 dual pairs, and present applications of our implementation to recent `graph logics'.
翻译:线性推论是布林代数的有效不平等,其中每个变量在每一侧最多出现一次。 等量地,它是布林术语的线性重写规则,它构成了有效的暗示。 线性推论在结构证据理论中发挥了重要作用, 特别是在结构下逻辑模型和深度推论系统标准化参数中。 在这项工作中, 我们利用最近开发的线性公式图形表达方式来构建一个能够更有效地搜索开关- 中间线性独立推论的实施。 我们用它来找出四个“ 最小” 8 独立可变的推论, 并证明不存在较小推论; 相比之下, 先前的一种方法直接基于公式, 已经达到7个变量的计算限度。 其中两种新的推论得出了以前发现的一些独立的线性推论。 另外两种( 双向) 展示结构似乎超出了我们所了解的先前方法的范围; 特别是, 它们的存在与Das 和 Strasburgurger 的推论有矛盾, 并且还证明我们最近独立的第 5号 中的所有双向性应用 。