Decision tactics for derivation search in the resolution method
The authors consider ordering tactics within the resolution method capable of establishing derivability of formulas from a decidable class of predicate calculus in which the condition of bounded term ranks has been weakened.
scientific article; zbMATH DE number 4085612