A simplified form of condensed detachment (Q1903086): Difference between revisions

The paper gives an attempt to define some version of the condensed detachment rule which is independent of the concept ``most general unifier''. Proving the equivalence of the introduced concept and the traditional one, the author uses the assertion that applying nontrivial substitution will increase the number of variable occurrences or decrease the number of distinct variables. This assertion contradicts a substitution \(\{f(y)/x\}\), where \(y\) is a new variable.