Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.

documentationgenericrlvarl

rlvarl – list of bound variables

Calling Sequence

rlvarl \((\,\varphi\,)\)

Arguments

\(\varphi\) first-order formula

Returns

\(\{L_f,\ L_b\}\) \(\{\)list of variables, list of variables\(\}\)

Description

Returns a pair of two lists \(L_f\) and \(L_b\), which are the sets of all variables that have a free or bound occurrence in \(\varphi\), respectively. Both \(L_f\) and \(L_b\) are sorted according to the Reduce kernel order.

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

Unless the formula is prenex it is possible to have \(L_f \cap L_b \neq \emptyset.\)

Example

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

See Also