A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. 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变量时已面临计算极限。其中两个新推理推导出了一些先前发现的独立线性推理,另外两个(互为对偶)展现出超越已知方法范畴的结构特征——其存在性尤其推翻了达斯和斯特拉斯布格尔的一个猜想。我们还识别出10个与前述所有推理独立的极小9变量线性推理(构成5组对偶对),并展示了该实现方法在最新“图逻辑”中的应用。