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个对偶对,并呈现了我们实现的在最近的“图逻辑”中的应用。