Associative Processing Techniques for Theorem-Proving.
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1972
- Accession Number
- AD0743313
Entities
People
- Rona Barbara Stillman
Organizations
- Rome Laboratory