## Calling Sequence

## 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- rlbrop
^{⊕}— bracket operators - rlsimpl
^{⊖}— implicitly call the standard simplifier on all interactive evaluation results

## See Also

- mkand — big conjunction for loop action
- mkor — big disjunction for loop action