Redlog Documentation Center

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

documentationgenerictrue

true, false, and, or, impl, repl, equiv, not, ex, all – Boolean operators and first-order quantifiers

Calling Sequence

true
false
\(\varphi_1\) and \(\dots\) and \(\varphi_n\)
\(\varphi_1\) or \(\dots\) or \(\varphi_n\)
\(\varphi_1\) impl \(\varphi_2\)
\(\varphi_1\) repl \(\varphi_2\)
\(\varphi_1\) equiv \(\varphi_2\)
not \(\varphi_1\)
ex \((\,x_1\,,\ \varphi_1\,)\)
ex \((\,\{x_1,\dots,x_m\}\,,\ \varphi_1\,)\)
all \((\,x_1\,,\ \varphi_1\,)\)
all \((\,\{x_1,\dots,x_m\}\,,\ \varphi_1\,)\)

Arguments

\(\varphi_1, \dots, \varphi_n\) first-order formulas
\(x_1, \dots, x_m\) variables

Returns

\(\varphi′\) first-order formula

Description

Boolean operators are used to construct quantifier-free formulas as syntactic objects based on true, false, and context-specific atomic formulas. First-order formulas are obtained by using in addition the first-order quantifiers ex and all. Note that no semantic evaluation takes place when using these operators and quantifiers. Some basic evaluations are performed by the standard simplifiers rlsimpl for the various domains. The switch rlsimpl can be turned on to implicitly apply rlsimpl to all interactive formula input.

Among the infix operators the precedence is and \(\succ\) or \(\succ\) impl \(\succ\) repl \(\succ\) equiv. The switch rlbrop can be turned off to save parentheses in Redlog based on those precedence rules.

and and or, in contrast to impl, repl, and equiv what Reduce calls nary operators. That is, they can talk an arbitrary number \(n\geq2\) of arguments. Nested occurrences of nary operators are technically possible but are typically flattened by the standard simplifiers for the various domains. For convenience the quantifiers admit as their first argument lists of variables, which are implicitly expanded into nested quantifiers with single variable arguments.

There are for loop actions mkand and mkor for systematically constructing big conjunctions and disjunctions.

Examples

all(x, ex(y, x^2 + x*y + b > 0 and x + a*y^2 + b <= 0));
phiprime := all({x, y}, x < y impl ex(z, x < z < y));

Switches

⊕ = on by default, ⊖ = off by default

See Also