Redlog Documentation Center

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

documentationgenericrlall

rlall – universal closure

Calling Sequence

rlall \((\,\varphi\,)\)
rlall \((\,\varphi\,,\ L\,)\)

Arguments

\(\varphi\) first-order formula
\(L\) list of variables

Returns

\(\varphi′\) first-order formula

Description

Universally quantify all variables with free occurrences inside \(\varphi\). The optional argument \(L\) is an exception list, i.e., variables in \(L\) remain unquantified.

For positively specifying a list of variables to be quantified use the universal quantifier all with the corresponding list as its first argument.

Examples

rlall(a=0 or b=0 or all(a, ex({c, d}, c > a and a > b and b > d), {b});

See Also