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.
Example
For example, in term rewriting, before applying a rule to a given term , each variable in should be replaced by a fresh one to avoid clashes with variables occurring in . Given the rule
and the term
, attempting to find a matching substitution of the rule's left-hand side, , within will fail, since cannot match . However, if the rule is replaced by a fresh copy
before, matching will succeed with the answer substitution .