Application of the strategy of ordering disjunctives for a modification of the method of resolutions (Q1115413)

A complete strategy was formulated in the author's earlier paper [Issled. Prikl. Mat. 2, 85-90 (1974; Zbl 0341.68060)] for searching for a proof in the resolution method, enabling us to establish the provability of formulas in a one-place predicate calculus, such that the ranks of terms occurring in disjunctives of the proof are not greater than 1. This strategy depends on the ordering U of literals in disjunctives, satisfying the following condition: (A) for any literals X and Y, if the literal X precedes Y in U, then for any substitution \(\sigma\), the literal \(X\sigma\) precedes \(Y\sigma\) in U. If such an ordering U is known, then we establish the provability of formulas in the predicate calculus by the resolution method in such a way that we first eliminate those literals which do not precede the other literals in the disjunctives containing them.