Enumerating Independent Linear Inferences

DOI10.46298/LMCS-19(2:11)2023MaRDI QIDQ6135760zbMATH OpenFDO

Authors Anupam Das

Publication date 26 August 2023

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2111.05209

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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

Cites work

• scientific article; zbMATH DE number 3583767 (Why is no real title available?)
• scientific article; zbMATH DE number 1980939 (Why is no real title available?)
• scientific article; zbMATH DE number 7594103 (Why is no real title available?)
• A Characterization of Medial as Rewriting Rule
• A Local System for Classical Logic
• A game semantics for linear logic
• A system of interaction and structure
• Algorithm 457: finding all cliques of an undirected graph
• An Analytic Propositional Proof System on Graphs
• Coherent interaction graphs
• Complement reducible graphs
• Extension without cut
• Introduction to computability logic
• Linear logic
• Logic beyond formulas: a proof system on graphs
• New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial
• No complete linear term rewriting system for propositional logic
• Normalisation Control in Deep Inference via Atomic Flows
• On linear rewriting systems for Boolean logic and some applications to proof theory
• On the relative proof complexity of deep inference via atomic flows
• Rewriting with linear inferences in propositional logic
• The relative efficiency of propositional proof systems

Cited in

(1)

• Inference of Uniquely Terminating EML

This page was built for publication: Enumerating Independent Linear Inferences

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135760)