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组对偶对),并展示了该实现在此前“图逻辑”中的应用。