Redlog Documentation Center

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

documentationgenericrlex

rlex – existential closure

Calling Sequence

rlex \((\,\varphi\,)\)
rlex \((\,\varphi\,,\ L\,)\)

Arguments

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

Returns

\(\varphi′\) first-order formula

Description

Existentially 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 existential quantifier ex with the corresponding list as its first argument.

Examples

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

See Also