LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INSTANCE

Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER

Let p and q be terms or formulas (there is no difference in ACL2). Then we say p is an instance or substitution instance of q if and only if p can be obtained from q by uniformly replacing the variables of q by terms. Sometimes we call p the target and q the pattern because by choosing appropriate replacements we can make the pattern match many different targets.

For example, the following target is an instance of the given pattern:

target:      (APP (APP (REV A) (REV B)) (REV C))
pattern:     (APP (APP   x       y    ) (REV z))

The replacement or substitution used in this match of the pattern to the target is:

variable in pattern          replacement term
x                              (REV A) 
y                              (REV B)
z                              C

((x  (REV A))
 (y  (REV B))
 (z  C)).

Please use your browser's Back Button to return to the page that mentioned ``instance.''