Enumerating Independent Linear Inferences
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-i...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2023-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/8695/pdf |
| _version_ | 1797268448465649664 |
|---|---|
| author | Anupam Das Alex Rice |
| author_facet | Anupam Das Alex Rice |
| author_sort | Anupam Das |
| collection | DOAJ |
| description | 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'. |
| first_indexed | 2024-04-25T01:32:38Z |
| format | Article |
| id | doaj.art-b2746e7b186446b1a671dbdfb19cafd4 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:32:38Z |
| publishDate | 2023-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b2746e7b186446b1a671dbdfb19cafd42024-03-08T10:59:15ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742023-05-01Volume 19, Issue 210.46298/lmcs-19(2:11)20238695Enumerating Independent Linear InferencesAnupam DasAlex RiceA 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'.https://lmcs.episciences.org/8695/pdfcomputer science - logic in computer science |
| spellingShingle | Anupam Das Alex Rice Enumerating Independent Linear Inferences Logical Methods in Computer Science computer science - logic in computer science |
| title | Enumerating Independent Linear Inferences |
| title_full | Enumerating Independent Linear Inferences |
| title_fullStr | Enumerating Independent Linear Inferences |
| title_full_unstemmed | Enumerating Independent Linear Inferences |
| title_short | Enumerating Independent Linear Inferences |
| title_sort | enumerating independent linear inferences |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/8695/pdf |
| work_keys_str_mv | AT anupamdas enumeratingindependentlinearinferences AT alexrice enumeratingindependentlinearinferences |