One modification of the ordering strategy in the resolution method (Q1115411)

One of the simplest deduction search strategies in the resolution method is the strategy with ordering developed by \textit{I. R. Slagle} [J. Assoc. Comput. Mach. 14, 687-697 (1967; Zbl 0157.024)] and \textit{S. Yu. Maslov} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 16, 126-136 (1969; Zbl 0206.291)]. The ordering strategy restricts the choice of the principal terms for the application of the resolution rule (the R rule). In some cases, this reduces the complexity of deductions and produces decision algorithms for some decidable classes of predicate calculus. In this note, we consider a modification of the ordering strategy and its application to the construction of a decision algorithm for one class of formulas in the predicate calculus.