Redlog Documentation

documentationgenericrlfvarl
rlfvarl – list of free variables

Calling Sequence

rlfvarl \((\,\varphi\,)\)

Arguments

\(\varphi\) first-order formula

Returns

\(L\) list of variables

Description

Returns the set of all variables that have a free occurrence in \(\varphi\) as a list. \(L\) is sorted according to the Reduce kernel order.

An occurrence of a variable is an occurrence inside an atomic formula. A free occurrence is an occurrence that is not within the scope of a corresponding quantifier. Note that by this definition, variables that are quantified but do not appear in any atomic formula do not occur at all.

Example

rlfvarl(ex({w, x, y, z}, v=0 and x=0 and y=0) and w=0 and y=0);

See Also