Anupam Das ; Alex Rice - Enumerating Independent Linear Inferences

lmcs:8695 - Logical Methods in Computer Science, May 19, 2023, Volume 19, Issue 2 - https://doi.org/10.46298/lmcs-19(2:11)2023
Enumerating Independent Linear InferencesArticle

Authors: Anupam Das ; Alex Rice

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'.


Volume: Volume 19, Issue 2
Secondary volumes: Selected Papers of the 6th International Conference on Formal Structures and Deduction (FSCD 2021)
Published on: May 19, 2023
Accepted on: March 23, 2023
Submitted on: November 10, 2021
Keywords: Computer Science - Logic in Computer Science

Classifications

Mathematics Subject Classification 20201

Consultation statistics

This page has been seen 3440 times.
This article's PDF has been downloaded 502 times.