In Anupam’s recent post, he introduced the linear inferences switch and medial. By computational search it had been shown that all linear inferences with 6 or fewer variables are derivable from these two inferences. He also gave an 8 variable linear inference which is not derivable from switch and medial and posed the question of…
Tag: open problem
A new linear inference of size 8
Linear inferences are propositional tautologies of the form , where and are formulas with at most one occurrence of each propositional variable. These form a -complete set, but surprisingly little is known about their structure, despite their importance in structural proof theory (and beyond). In this post I will cover some of the background on…