Condensed detachment is complete for relevance logic: A computer-aided proof (Q1181717)

The condensed detachment rule \(D\) is a combination of modus ponens with a minimal amount of substitution. Earlier \(D\) has been shown to be complete for intuitionistic and classical implicational logic but incomplete for \(BCK\) and \(BCI\) logic. We show that \(D\) is complete for the relevance logic. One of the main steps is the proof of the formula \(((a\to a)\to a)\to a\) found in interaction with our resolution theorem prover. Various strategies of generating consequences of the axioms and choosing best ones for the next iteration were tried until the proof was found.