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.
The concept is often used without explanation.
Fresh variables may be used to replace other variables, to eliminate variable shadowing or capture. 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. 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.
Example.
For example, in term rewriting, before applying a rule formula_1 to a given term formula_2, each variable in formula_1 should be replaced by a fresh one to avoid clashes with variables occurring in formula_2.
Given the rule
formula_5
and the term 
formula_6,
attempting to find a matching substitution of the rule's left-hand side, formula_7, within formula_6 will fail, since formula_9 cannot match formula_10.
However, if the rule is replaced by a "fresh copy"
formula_11 
before, matching will succeed with the answer substitution formula_12.
References.
 ;templatestyles src="Reflist/styles.css" / ;