The Concept of Weak Substitution in Theorem-Proving

Abstract

Many of the centrally important predicates which occur within theorem-proving programs involve, in their computation, a subcalculation aimed at determining whether or not a substitution exists satisfying certain constraints. Some of the principal difficulties in achieving efficient theorem-proving programs are traceable to the amount of computation required by this “substitution-existence analysis.” In this investigation, the concept of “weak substitution” is introduced and its utility and applicability in the subsumption and unification computations are examined. The main motivation for considering weak substitutions is this: the existence of a weak substitution having certain properties is relatively easy to detect, whereas the existence of a substitution proper having the same properties is not. Furthermore, the absence of such a weak substitution is a sufficient condition for the absence of the substitution proper. Using the concept of weak substitution, a particularly efficient implementation of the subsumption and unification computations on an associative processor is presented. © 1973, ACM. All rights reserved.