Fresh variable: Difference between revisions

Revision as of 18:30, 28 June 2023

Revision as of 18:50, 28 June 2023

Line 1:

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.{{cn|date=June 2023}}

== Example ==

For example, in [[term rewriting]], before applying a rule <math>l \to r</math> to a given term <math>t</math>, each variable in <math>l \to r</math> should be replaced by a fresh one to avoid clashes with variables occurring in <math>t</math>.{{cn|date=June 2023}}

Given the rule

:<math>append(cons(x,y),z) \to cons(x,append(y,z))</math>