Accession Number : AD0743313

Title :   Associative Processing Techniques for Theorem-Proving.

Descriptive Note : Doctorial thesis,

Corporate Author : ROME AIR DEVELOPMENT CENTER GRIFFISS AFB N Y

Personal Author(s) : Stillman,Rona Barbara

Report Date : APR 1972

Pagination or Media Count : 104

Abstract : A substitution theta is an operation which can be performed on an expression E whereby (1) each occurrence of a variable in E is replaced by an occurrence of some term; (2) all occurrences of the same variable are replaced by occurrences of the same term. It is possible that in (1), the term and the variable of which it replaces an occurrence, should be the same; i.e. that some occurrences of a variable x should be 'left alone' by the substitution. In that case, by (2), all occurrences of x must be. In this investigation one asks what happens if condition (2) is dropped. Operations which satisfy (1) but not necessarily (2) are called weak substitutions. Any notions (e.g., subsumption, unification, resolution) in which substitutions play a part generalize correspondingly. (Author)

Descriptors :   (*COMPUTER PROGRAMMING, *MATHEMATICAL LOGIC), PATTERN RECOGNITION, MEMORY DEVICES, THEOREMS, PROBLEM SOLVING, ITERATIONS, THESES

Subject Categories : Theoretical Mathematics
      Computer Programming and Software
      Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE