# 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):

# Report Date:

## 1972-04-01

# Pagination or Media Count:

## 104.0

# 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:

# Subject Categories:

- Theoretical Mathematics
- Computer Programming and Software
- Computer Hardware