
Accession Number : AD0743313
Title : Associative Processing Techniques for TheoremProving.
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