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: deep inference
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…
Checking proofs with very low complexity
The very notion of mathematical proof is founded upon the idea that a proof is ‘routine’ to check. While it may be difficult to actually prove a mathematical theorem, a proof should allow us to verify its truth . But exactly how much effort is required to check a proof, in terms of computational complexity?…
