The Concept of Weak Substitution in Theorem-Proving

16Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

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.

Cite

CITATION STYLE

APA

Stillman, R. B. (1973). The Concept of Weak Substitution in Theorem-Proving. Journal of the ACM (JACM), 20(4), 648–667. https://doi.org/10.1145/321784.321792

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free