In formal reasoning, in particular in mathematical logic, computer algebra, and automated theorem proving, a fresh variable is a variable that did not occur in the context considered so far.
[1][citation needed] The concept is often used without explanation.
For instance, in alpha-conversion, the processing of terms in the lambda calculus into equivalent terms with renamed variables, replacing variables with fresh variables can be helpful as a way to avoid accidentally capturing variables that should be free.
[3] Another use for fresh variables involves the development of loop invariants in formal program verification, where it is sometimes useful to replace constants by newly introduced fresh variables.
[4] For example, in term rewriting, before applying a rule
should be replaced by a fresh one to avoid clashes with variables occurring in
[citation needed] Given the rule and the term attempting to find a matching substitution of the rule's left-hand side,
However, if the rule is replaced by a fresh copy[a] before, matching will succeed with the answer substitution
This logic-related article is a stub.