Saved in:
Bibliographic Details
Main Authors: Das, Anupam, Rice, Alex
Format: Preprint
Published: 2021
Subjects:
Online Access:https://arxiv.org/abs/2111.05209
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866914675955859456
author Das, Anupam
Rice, Alex
author_facet Das, Anupam
Rice, Alex
contents 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'.
format Preprint
id arxiv_https___arxiv_org_abs_2111_05209
institution arXiv
publishDate 2021
record_format arxiv
spellingShingle Enumerating Independent Linear Inferences
Das, Anupam
Rice, Alex
Logic in Computer Science
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'.
title Enumerating Independent Linear Inferences
topic Logic in Computer Science
url https://arxiv.org/abs/2111.05209