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变量时已触及计算极限。其中两个新推理推导出了一些先前发现的独立线性推理。另两个(对偶)推理展现的结构似乎超越了已知方法的适用范围;特别地,其存在性否定了Das与Strassburger的一个猜想。我们还识别出独立于上述所有推理的10个极小9变量线性推理(包含5组对偶对),并展示了本实现方法在近期"图逻辑"研究中的应用。