### Quick Start

In case you hate long manuals and want to see something within a
minute type `reduce` in the command line. reduce should start up.
Type the four commands `load redlog; rlset ofsf; phi :=
ex(x,a*x^2+b*x+1=0); rlqe phi;` and hit return. You will get a
condition on the parameters `a` and `b` such that the quadratic
polynomial `a*x^2+b*x+1` has a real root.

## Contents

## 1 Introduction

redlog stands for reduce* logic system*. It provides an
extension of the computer algebra system reduce to a *computer
logic system* implementing symbolic algorithms on first-order formulas
wrt. temporarily fixed first-order languages and theories.

This document serves as a user guide describing the usage of redlog from the algebraic mode of reduce. For a detailed description of the system design see [DS97a].

An overview on some of the application areas of redlog is given in [DSW98]. See also References for articles on redlog applications.

### 1.1 Contexts

redlog is designed for working with several languages and theories in the sense of first-order logic. Both a language and a theory make up a context. In addition, a context determines the internal representation of terms. There are the following contexts available:

- ofsf
- of stands for
*ordered fields*, which is a little imprecise. The quantifier elimination actually requires the more restricted class of*real closed fields*, while most of the tool-like algorithms are generally correct for ordered fields. One usually has in mind real numbers with ordering when using ofsf. - dvfsf
*Discretely valued fields*. This is for computing with formulas over classes of p-adic valued extension fields of the rationals, usually the fields of p-adic numbers for some prime p.- acfsf
*Algebraically closed fields*such as the complex numbers.- pasf
*Presburger Arithmetic*, i.e., the linear theory of integers with congruences modulo m for m>=2 .- ibalp
*Initial Boolean algebras*, basically quantified propositional logic.- dcfsf
*Differentially closed fields*according to Robinson. There is no natural example. The quantifier elimination is an optimized version of the procedure by Seidenberg (1956).

The trailing "-sf" stands for *standard form*, which is the
representation chosen for the terms within the implementation.
Accordingly, "-lp" stands for *Lisp prefix*.
See Context Selection, for details on selecting redlog
contexts.

### 1.2 Overview

redlog origins from the implementation of quantifier elimination procedures. Successfully applying such methods to both academic and real-world problems, the authors have developed over the time a large set of formula-manipulating tools, many of which are meanwhile interesting in their own right:

- Numerous tools for comfortably inputing, decomposing, and
analyzing formulas. This includes, for instance, the construction of
systematic formulas via
`for`

-loops, and the extension of built-in commands such as`sub`

or`part`

. See Format and Handling of Formulas. - Several techniques for the
*simplification*of formulas. The simplifiers do not only operate on the boolean structure of the formulas but also discover algebraic relationships. For this purpose, we make use of advanced algebraic concepts such as Groebner basis computations. For the notion of simplification and a detailed description of the implemented techniques for the contexts ofsf and acfsf see [DS97]. For the dvfsf context see [DS99]. See Simplification. - Various
*normal form computations*. The cnf*/*dnf computation includes both boolean and algebraic simplification strategies [DS97]. The*prenex normal form*computation minimizes the number of quantifier changes. See Normal Forms. *Quantifier elimination*computes quantifier-free equivalents for given first-order formulas.For ofsf and dvfsf we use a technique based on elimination set ideas [Wei88]. The ofsf implementation is restricted to at most quadratic occurrences of the quantified variables, but includes numerous heuristic strategies for coping with higher degrees. See [LW93], [Wei97], for details on the method. The dvfsf implementation is restricted to formulas that are linear in the quantified variables. The method is described in detail in [Stu00].

The acfsf quantifier elimination is based on

*comprehensive Groebner basis*computation. There are no degree restrictions for this context [Wei92]. See Quantifier Elimination.- The contexts ofsf
and acfsf
allow a variant of quantifier
elimination called generic quantifier elimination
[DSW98].
There are certain non-degeneracy assumptions made on the parameters,
which considerably speeds up the elimination.
For geometric theorem proving it has turned out that these assumptions correspond to reasonable geometric non-degeneracy conditions [DSW98]. Generic quantifier elimination has turned out useful also for physical applications such as network analysis [Stu97]. There is no generic quantifier elimination available for dvfsf. See Generic Quantifier Elimination.

- The contexts ofsf and dvfsf provide variants of (generic) quantifier elimination that additionally compute answers such as satisfying sample points for existentially quantified formulas. This has been referred to as the "extended quantifier elimination problem" [Wei97a]. See Quantifier Elimination.
- ofsf
includes linear
*optimization*techniques based on quantifier elimination [Wei94a]. See Linear Optimization.

### 1.3 Conventions

To avoid ambiguities with other packages, all redlog functions and
switches are prefixed by "`rl`

". The remaining part of the name is
explained by the first sentence of the documentation of the single
functions and switches.

Some of the numerous switches of redlog have been introduced only for finding the right fine tuning of the functions, or for internal experiments. They should not be changed anymore, except for in very special situations. For an easier orientation the switches are divided into three categories for documentation:

- Switch
- This is an ordinary switch, which usually selects strategies appropriate
for a particular input, or determines the required trade-off between
computation-speed and quality of the result.
- Advanced Switch
- They are used like ordinary switches. You need, however, a good
knowledge about the underlying algorithms for making use of it.
- Fix Switch
- You do not want to change it.

## 2 Loading and Context Selection

### 2.1 Loading Redlog

At the beginning of each session redlog has to be loaded
explicitly. This is done by inputing the command ```
load_package
redlog;
```

from within a reduce session.

### 2.2 Context Selection

Fixing a context reflects the mathematical fact that first-order formulas are defined over fixed languages specifying, e.g., valid function symbols and relation symbols (predicates). After selecting a language, fixing a theory such as "the theory of ordered fields", allows to assign a semantics to the formulas. Both language and theory make up a redlog context. In addition, a context determines the internal representation of terms.

As first-order formulas are not defined unless the language is known, and meaningless unless the theory is known, it is impossible to enter a first-order formula into redlog without specifying a context:

REDUCE 3.6, 15-Jul-95, patched to 30 Aug 98 ... 1: load_package redlog; 2: f := a=0 and b=0; ***** select a context

See Contexts, for a summary of the available contexts ofsf,
dvfsf,
acfsf,
pasf,
ibalp
and dcfsf.
A context can be selected by the `rlset`

command:

**rlset**[

`context`[

`arguments...`]]

— Function:

**rlset**

`argument-list`

Set current context. Valid choices for

contextare ofsf (ordered fields standard form), dvfsf (discretely valued fields standard form), acfsf (algebraically closed fields standard form), pasf (Presburger arithmetic standard form), ibalp (initial Boolean algebra Lisp prefix), and dcfsf. With ofsf, acfsf, pasf, ibalp, and dcfsf there are no further arguments. With dvfsf an optionaldvf_class_specificationcan be passed, which defaults to`0`

.`rlset`

returns the old setting as a list that can be saved to be passed to`rlset`

later. When called with no arguments (or the empty list),`rlset`

returns the current setting.

**dvf_class_specification**

Zero, or a possibly negative prime q.

For q=0 all computations are uniformly correct for all p-adic valuations. Both input and output then possibly involve a symbolic constant "p", which is being reserved.

For positive q, all computations take place wrt. the corresponding q-adic valuation.

For negative q, the "-" can be read as “up to”, i.e., all computations are performed in such a way that they are correct for all p-adic valuations with p <= q. In this case, the knowledge of an upper bound for p supports the quantifier elimination

`rlqe`

/`rlqea`

[Stu00]. See Quantifier Elimination.

The user will probably have a "favorite" context reflecting their
particular field of interest.
To save the explicit declaration of the
context with each session, redlog provides a global variable
`rldeflang`

, which contains a default context. This variable can be
set already *before* loading `redlog`. This is typically done
within the `.reducerc` profile:

lisp (rldeflang!* := '(ofsf));

Notice that the Lisp list representation has to be used here.

**rldeflang!***

Default language. This can be bound to a default context before loading

redlog. More precisely,`rldeflang!*`

contains the arguments of`rlset`

as a Lisp list. If`rldeflang!*`

is non-nil,`rlset`

is automatically executed on`rldeflang!*`

when loadingredlog.

In addition, redlog evaluates an environment variable
`RLDEFLANG`

. This allows to fix a default context within the shell
already before starting reduce. The syntax for setting environment
variables depends on the shell. For instance, in the gnu Bash or in
the csh shell one would say `export RLDEFLANG=ofsf`

or
`setenv RLDEFLANG ofsf`

, respectively.

**RLDEFLANG**

Default language. This may be bound to a context in the sense of the first argument of

`rlset`

. With`RLDEFLANG`

set, any`rldeflang!*`

binding is overloaded.

## 3 Format and Handling of Formulas

After loading redlog and selecting a context (see Loading and Context Selection), there are *first-order formulas* available as
an additional type of symbolic expressions. That is, formulas are now
subject to symbolic manipulation in the same way as, say, polynomials or
matrices in conventional systems. There is nothing changed in the
behavior of the builtin facilities and of other packages.

### 3.1 First-order Operators

Though the operators `and`

, `or`

, and `not`

are already
sufficient for representing boolean formulas, redlog provides a
variety of other boolean operators for the convenient mnemonic input of
boolean formulas.

**not**

— n-ary Infix Operator:

**and**

— n-ary Infix Operator:

**or**

— Binary Infix Operator:

**impl**

— Binary Infix Operator:

**repl**

— Binary Infix Operator:

**equiv**

The infix operator precedence is from strongest to weakest:

`and`

,`or`

,`impl`

,`repl`

,`equiv`

.

See Extended Built-in Commands, for the description of extended
`for`

-loop
actions that allow to comfortably input large systematic
conjunctions and disjunctions.

reduce expects the user to know about the precedence of `and`

over `or`

. In analogy to `+`

and `*`

, there are thus no
parentheses output around conjunctions within disjunctions. The
following switch causes such subformulas to be bracketed anyway.
See Conventions, for the notion of a "fix switch".

**rlbrop**

Bracket all operators. By default this switch is on, which causes some private printing routines to be called for formulas: All subformulas are bracketed completely making the output more readable.

Besides the boolean operators introduced above, first-order logic
includes the well-known existential quantifiers and universal
quantifiers
"*exists*" and "*forall*".

**ex**

— Binary Operator:

**all**

These are the quantifiers. The first argument is the quantified variable, the second one is the matrix formula. Optionally, one can input a list of variables as first argument. This list is expanded into several nested quantifiers.

See Closures, for automatically quantifying all variables except for an exclusion list.

**bex**

— Binary Operator:

**ball**

These are the bounded quantifiers. The first argument is the quantified variable, the second one is the bound and the third one is the matrix formula. A bound is a quantifier-free formula, which contains only one variable and defines a finite set. Formulas with bounded quantifiers are only available in pasf.

For convenience, we also have boolean constants for the truth values.

**true**

— Variable:

**false**

These algebraic mode variables are reserved. They serve as truth values.

### 3.2 Closures

**rlall**

`formula`[

`exceptionlist`]

Universal closure.

exceptionlistis a list of variables empty by default. Returnsformulawith all free variables universally quantified, except for those inexceptionlist.

**rlex**

`formula`[

`exceptionlist`]

Existential closure.

exceptionlistis a list of variables empty by default. Returnsformulawith all free variables existentially quantified, except for those inexceptionlist.

### 3.3 OFSF Operators

The ofsf
context implements *ordered fields* over the language of
*ordered rings*. Proceeding this way is very common in model theory
since one wishes to avoid functions which are only partially defined,
such as division in the language of ordered fields. Note that the
ofsf quantifier elimination procedures
(see Quantifier Elimination and Variants) for non-linear formulas
actually operate over
*real closed fields*. See Contexts and Context Selection for details on contexts.

**equal**

— Binary Infix operator:

**neq**

— Binary Infix operator:

**leq**

— Binary Infix operator:

**geq**

— Binary Infix operator:

**lessp**

— Binary Infix operator:

**greaterp**

The above operators may also be written as

`=`

,`<>`

,`<=`

,`>=`

,`<`

, and`>`

, respectively. For ofsf there is specified that all right hand sides must be zero. Non-zero right hand sides in the input are hence subtracted immediately to the corresponding left hand sides. There is a facility to inputchainsof the above relations, which are also expanded immediately:a<>b<c>d=f => a-b <> 0 and b-c < 0 and c-d > 0 and d-f = 0Here, only adjacent terms are related to each other.

Though we use the language of ordered rings, the input of integer
reciprocals is allowed and treated correctly interpreting them as
constants for rational numbers.
There are two switches that allow to
input arbitrary reciprocals, which are then resolved into proper
formulas in various reasonable ways. The user is welcome to experiment
with switches like the following, which are not marked as *fix
switches*. See Conventions, for the classification of redlog
switches.

**rlnzden**

— Switch:

**rlposden**

Non-zero/positive denominators. Both switches are off by default. If both

`rlnzden`

and`rlposden`

are on, the latter is active. Activating one of them, allows the input of reciprocal terms. With`rlnzden`

on, these terms are assumed to be non-zero, and resolved by multiplication. When occurring with ordering relations the reciprocals are resolved by multiplication with their square preserving the sign.(a/b)+c=0 and (a/d)+c>0; 2 => a + b*c = 0 and a*d + c*d > 0Turning

`rlposden`

on, guarantees the reciprocals to be strictly positive which allows simple, i.e. non-square, multiplication also with ordering relations.(a/b)+c=0 and (a/d)+c>0; => a + b*c = 0 and a + c*d > 0

The non-zeroness or positivity assumptions made by using the above
switches can be stored in a variable, and then later be passed as a
`theory`
(see theory) to certain redlog procedures.
Optionally, the system can be forced to add them to the formula at the
input stage:

**rladdcond**

Add condition. This is off by default. With

`rladdcond`

on, non-zeroness and positivity assumptions made due to the switches`rlnzden`

and`rlposden`

are added to the formula at the input stage. With`rladdcond`

and`rlposden`

on we get for instance:(a/b)+c=0 and (a/d)+c>0; => (b <> 0 and a + b*c = 0) and (d > 0 and a + c*d > 0)

### 3.4 DVFSF Operators

Discretely valued fields are implemented as a one-sorted language using
the operators `|`

, `||`

, `~`

, and `/~`

, which encode
`<=`

, `<`

, `=`

, and `<>`

in the value group, respectively. For details see
[Wei88], [Stu00], or [DS99].

**equal**

— Binary Infix operator:

**neq**

— Binary Infix operator:

**div**

— Binary Infix operator:

**sdiv**

— Binary Infix operator:

**assoc**

— Binary Infix operator:

**nassoc**

The above operators may also be written as

`=`

,`<>`

,`|`

,`||`

,`~`

, and`/~`

, respectively. Integer reciprocals in the input are resolved correctly. dvfsf allows the input ofchainsin analogy to ofsf. See OFSF Operators, for details.

With the dvfsf operators there is no treatment of parametric denominators available.

### 3.5 ACFSF Operators

**equal**

— Binary Infix operator:

**neq**

The above operators may also be written as

`=`

,`<>`

. As for ofsf, it is specified that all right hand sides must be zero. In analogy to ofsf, acfsf allows also the input ofchainsand an appropriate treatment of parametric denominators in the input. See OFSF Operators, for details.

Note that the switch `rlposden`

(see OFSF Operators) makes no
sense for algebraically closed fields.

### 3.6 PASF Operators

**equal**

— Binary Infix operator:

**neq**

— Binary Infix operator:

**leq**

— Binary Infix operator:

**geq**

— Binary Infix operator:

**lessp**

— Binary Infix operator:

**greaterp**

The above operators may also be written as

`=`

,`<>`

,`<=`

,`>=`

,`<`

, and`>`

, respectively. — Ternary Prefix operator:cong

— Ternary Prefix operator:ncong

The operators cong and ncong represent congruences with nonparametric modulus given by the third argument. The example below defines the set of even integers.

f := cong(x,0,2); => x ~2~ 0As for ofsf, it is specified that all right hand sides are transformed to be zero. In analogy to ofsf, pasf allows also the input of

chainsSee OFSF Operators, for details.

### 3.7 IBALP Operators

**bnot**

— n-ary Infix operator:

**band**

— n-ary Infix operator:

**bor**

— Binary Infix operator:

**bimpl**

— Binary Infix operator:

**brepl**

— Binary Infix operator:

**bequiv**

The operator

`bnot`

may also be written as`~`

. The operators`band`

and`bor`

may also be written as`&`

and`|`

, resp. The operators`bimpl`

,`brepl`

, and`bequiv`

may be written as`->`

,`<-`

, and`<->`

, resp.

### 3.8 DCFSF Operators

**d**

The operator

`d`

denotes (higher) derivatives in the sense of differential algebra. For instance, the differential equationx'^2 + x = 0is input as

`x d 1 ** 2 + x = 0`

.`d`

binds stronger than all other operators.

**equal**

— Binary Infix operator:

**neq**

The operator

`equal`

may also be written as`=`

. The operator`neq`

may also be written as`<>`

.

### 3.9 Extended Built-in Commands

Systematic conjunctions and disjunctions can be constructed in the
algebraic mode in analogy to, e.g., `for ... sum ...`

:

**mkand**

— for loop action:

**mkor**

Make and/or. Actions for the construction of large systematic conjunctions/disjunctions via for loops.

for i:=1:3 mkand for j:=1:3 mkor if j<>i then mkid(x,i)+mkid(x,j)=0; => true and (false or false or x1 + x2 = 0 or x1 + x3 = 0) and (false or x1 + x2 = 0 or false or x2 + x3 = 0) and (false or x1 + x3 = 0 or x2 + x3 = 0 or false)

Here the truth values
come into existence due to the internal
implementation of `for`

-loops. They are always neutral in their
context, and can be easily removed via simplification (see function rlsimpl, see switch rlsimpl).

The reduce substitution command `sub`

can be applied to formulas using the usual syntax.

**substitution_list**

substitution_listis a list of equations each with a kernel left hand side.

**sub**

`substitution_list formula`

Substitute. Returns the formula obtained from

formulaby applying the substitutions given bysubstitution_list.sub(a=x,ex(x,x-a<0 and all(x,x-b>0 or ex(a,a-b<0)))); => ex x0 ( - x + x0 < 0 and all x0 ( - b + x0 > 0 or ex a (a - b < 0)))

`sub`

works in such a way that equivalent formulas remain equivalent after substitution. In particular, quantifiers are treated correctly.

**part**

`formula n1`[

`n2`[

`n3...`]]

Extract a part. The

`part`

offormulais implemented analogously to that for built-in types: in particular the 0th part is the operator.

See rlmatrix,
for extracting the *matrix part* of a formula, i.e., removing
*all* initial quantifiers.

**length**

`formula`

Length of

formula. This is the number of arguments to the top-level operator. The length is of particular interest with the n-ary operators`and`

and`or`

. Notice that`part(`

formula`,length(`

formula`))`

is the part of largest index.

Next: Basic Functions on Formulas, Previous: Extended Built-in Commands, Up: Format and Handling of Formulas

### 3.10 Global Switches

There are three global switches that do not belong to certain procedures, but control the general behavior of redlog.

**rlsimpl**

Simplify. By default this switch is off. With this switch on, the function

`rlsimpl`

is applied at the expression evaluation stage. See rlsimpl.

Automatically performing formula simplification at the evaluation stage is very similar to the treatment of polynomials or rational functions, which are converted to some normal form. For formulas, however, the simplified equivalent is by no means canonical.

**rlrealtime**

Real time. By default this switch is off. If on it protocols the wall clock time needed for redlog commands in seconds. In contrast to the built-in

`time`

switch, the time is printedabovethe result.

**rlverbose**

Verbose. By default this switch is off. It toggles verbosity output with some redlog procedures. The verbosity output itself is not documented.

### 3.11 Basic Functions on Formulas

**rlatnum**

`formula`

Number of atomic formulas. Returns the number of atomic formulas contained in

formula. Mind that truth values are not considered atomic formulas. In pasf the amount of atomic formulas in a bounded formula is computed syntactically without expanding the bounds.

**multiplicity_list**

A list of 2-element-lists containing an object and the number of its occurrences. Names of functions returning

multiplicity_liststypically end on "ml".

**rlatl**

`formula`

List of atomic formulas. Returns the set of atomic formulas contained in

formulaas a list.

**rlatml**

`formula`

Multiplicity list of atomic formulas. Returns the atomic formulas contained in

formulain amultiplicity_list.

**rlifacl**

`formula`

List of irreducible factors. Returns the set of all irreducible factors of the nonzero terms occurring in

formula.rlifacl(x**2-1=0); => {x + 1,x - 1}

**rlifacml**

`formula`

Multiplicity list of irreducible factors. Returns the set of all irreducible factors of the nonzero terms occurring in

formulain amultiplicity_list.

**rlterml**

`formula`

List of terms. Returns the set of all nonzero terms occurring in

formula.

**rltermml**

`formula`

Multiplicity list of terms. Returns the set of all nonzero terms occurring in

formulain amultiplicity_list.

**rlvarl**

`formula`

Variable lists. Returns both the list of variables occurring freely and that of the variables occurring boundly in

formulain a two-element list. Notice that the two member lists are not necessarily disjoint.

**rlfvarl**

`formula`

Free variable list. Returns the variables occurring freely in

formulaas a list.

**rlbvarl**

`formula`

Bound variable list. Returns the variables occurring boundly in

formulaas a list.

**rlstruct**

`formula`[

`kernel`]

Structure of a formula.

kernelis`v`

by default. Returns a list`{f,sl}`

.`f`

is constructed fromformulaby replacing each occurrence of a term with a kernel constructed by concatenating a number tokernel. Thesubstitution_list`sl`

contains all substitutions to obtainformulafrom`f`

.rlstruct(x*y=0 and (x=0 or y>0),v); => {v1 = 0 and (v2 = 0 or v3 > 0), {v1 = x*y,v2 = x,v3 = y}}

**rlifstruct**

`formula`[

`kernel`]

Irreducible factor structure of a formula.

kernelis`v`

by default. Returns a list`{f,sl}`

.`f`

is constructed fromformulaby replacing each occurrence of an irreducible factor with a kernel constructed by adding a number tokernel. The returnedsubstitution_list`sl`

contains all substitutions to obtainformulafrom`f`

.rlstruct(x*y=0 and (x=0 or y>0),v); => {v1*v2 = 0 and (v1 = 0 or v2 > 0), {v1 = x,v2 = y}}

## 4 Simplification

The goal of simplifying a first-order formula is to obtain an equivalent formula over the same language that is somehow simpler. redlog knows three kinds of simplifiers that focus mainly on reducing the size of the given formula: The standard simplifier, tableau simplifiers, and Groebner simplifiers. The ofsf versions of these are described in [DS97].

The acfsf versions are the same as the ofsf versions except for techniques that are particular to ordered fields such as treatment of square sums in connection with ordering relations.

For dvfsf
there is no Groebner simplifier available. The parts of the standard
simplifier that are particular to valued fields are described in
[DS99].
The tableau simplification is straightforwardly derived from the
*smart simplifications* described there.

In pasf only the standard simplifier is available.

Besides reducing the size of formulas, it is a reasonable simplification goal, to reduce the degree of the quantified variables. Our method of decreasing the degree of quantified variables is described for ofsf in [DSW98]. A suitable variant is available also in acfsf but not in dvfsf.

### 4.1 Standard Simplifier

The Standard Simplifier is a fast simplification algorithm that is
frequently called internally by other redlog algorithms. It can be
applied automatically at the expression evaluation stage by turning on
the switch `rlsimpl`

(see switch rlsimpl).

**rlsimpl**

`formula`[

`theory`]

Simplify.

formulais simplified recursively such that the result is equivalent under the assumption thattheoryholds. Default fortheoryis the empty theory`{}`

. Theory inconsistency may but need not be detected by`rlsimpl`

. Iftheoryis detected to be inconsistent, a corresponding error is raised. Note that under an inconsistent theory,anyformula is equivalent to the input, i.e., the result is meaningless.theoryshould thus be chosen carefully.

#### 4.1.1 General Features of the Standard Simplifier

The standard simplifier `rlsimpl`

includes the following features
common to all contexts:

- Replacement of atomic subformulas by simpler equivalents. These
equivalents are not necessarily atomic (switches
`rlsiexpl`

,`rlsiexpla`

, see General Standard Simplifier Switches). For details on the simplification on the atomic formula level, see OFSF-specific Simplifications, ACFSF-specific Simplifications, and DVFSF-specific Simplifications. - Proper treatment of truth values.
- Flattening
nested n-ary operator levels and resolving involutive
applications of
`not`

. - Dropping
`not`

operator with atomic formula arguments by changing the relation of the atomic formula appropriately. The languages of all contexts allow to do so. - Changing
`repl`

to`impl`

. - Producing a canonical ordering
among the atomic formulas on a given
level (switch
`rlsisort`

, see General Standard Simplifier Switches). - Recognizing equal subformulas
on a given level (switch
`rlsichk`

, see General Standard Simplifier Switches). - Passing down information that is collected during recursion (switches
`rlsism`

,`rlsiidem`

, see General Standard Simplifier Switches). The technique of implicit theories used for this is described in detail in [DS97], for ofsf/acfsf, and in [DS99], for dvfsf. - Considering interaction of atomic formulas on the same level and
interaction with information inherited from higher levels (switch
`rlsism`

, see General Standard Simplifier Switches). The smart simplification techniques used for this are beyond the scope of this manual. They are described in detail in [DS97], for ofsf/acfsf, and in [DS99], for dvfsf.

Next: OFSF-specific Simplifications, Previous: General Features of the Standard Simplifier, Up: Standard Simplifier

#### 4.1.2 General Standard Simplifier Switches

**rlsiexpla**

Simplify explode always. By default this switch is on. It is relevant with simplifications that allow to split one atomic formula into several simpler ones. Consider, e.g., the following simplification toggled by the switch

`rlsipd`

(see OFSF-specific Standard Simplifier Switches). With`rlsiexpla`

on, we obtain:f := (a - 1)**3 * (a + 1)**4 >=0; 7 6 5 4 3 2 => a + a - 3*a - 3*a + 3*a + 3*a - a - 1 >= 0 rlsimpl f; => a - 1 >= 0 or a + 1 = 0With

`rlsiexpla`

off,`f`

will simplify as in the description of the switch`rlsipd`

.`rlsiexpla`

is not used in the dvfsf context. The dvfsf simplifier behaves like`rlsiexpla`

on.

**rlsiexpl**

Simplify explode. By default this switch is on. Its role is very similar to that of

`rlsiexpla`

, but it considers the operator the scope of which the atomic formula occurs in: With`rlsiexpl`

on7 6 5 4 3 2 a + a - 3*a - 3*a + 3*a + 3*a - a - 1 >= 0simplifies as in the description of the switch

`rlsiexpla`

whenever it occurs in a disjunction, and it simplifies as in the description of the switch`rlsipd`

(see OFSF-specific Standard Simplifier Switches) else.`rlsiexpl`

is not used in the dvfsf context. The dvfsf simplifier behaves like`rlsiexpla`

on.

The user is not supposed to alter the settings of the following
*fix switches* (see Conventions):

**rlsism**

Simplify smart. By default this switch is on. See the description of the function

`rlsimpl`

(see Standard Simplifier) for its effects.rlsimpl(x>0 and x+1<0); => false

**rlsichk**

Simplify check. By default this switch is on enabling checking for equal sibling subformulas:

rlsimpl((x>0 and x-1<0) or (x>0 and x-1<0)); => (x>0 and x-1<0)

**rlsiidem**

Simplify idempotent. By default this switch is on. It is relevant only with switch

`rlsism`

on. Its effect is that`rlsimpl`

(see Standard Simplifier) is idempotent in the very most cases, i.e., an application of`rlsimpl`

to an already simplified formula yields the formula itself.

**rlsiso**

Simplify sort. By default this switch is on. It toggles the sorting of the atomic formulas on the single levels.

rlsimpl((a=0 and b=0) or (b=0 and a=0)); => a = 0 and b = 0

Next: OFSF-specific Standard Simplifier Switches, Previous: General Standard Simplifier Switches, Up: Standard Simplifier

#### 4.1.3 OFSF-specific Simplifications

In the ofsf context, the atomic formula simplification includes the following:

- Evaluation of variable-free atomic formulas to truth values.
- Make the left hand sides primitive over the integers with positive head coefficient.
- Evaluation of trivial square sums
to truth values (switch
`rlsisqf`

, see OFSF-specific Standard Simplifier Switches). Additive splitting of trivial square sums (switch`rlsitsqspl`

, see OFSF-specific Standard Simplifier Switches). - In ordering inequalities,
perform parity decomposition
(similar to squarefree decomposition) of terms (switch
`rlsipd`

, see OFSF-specific Standard Simplifier Switches) with the option to split an atomic formula multiplicatively into two simpler ones (switches`rlsiexpl`

and`rlsiexpla`

, see General Standard Simplifier Switches). - In equations and non-ordering inequalities,
replace left hand sides by their squarefree parts
(switch
`rlsiatdv`

, see OFSF-specific Standard Simplifier Switches). Optionally, perform factorization of equations and inequalities (switch`rlsifac`

, see OFSF-specific Standard Simplifier Switches, switches`rlsiexpl`

and`rlsiexpla`

, see General Standard Simplifier Switches).

For further details on the simplification in ordered fields see the article [DS97].

Next: ACFSF-specific Simplifications, Previous: OFSF-specific Simplifications, Up: Standard Simplifier

#### 4.1.4 OFSF-specific Standard Simplifier Switches

**rlsipw**

Simplification prefer weak orderings. Prefers weak orderings in contrast to strict orderings with implicit theory simplification.

`rlsipw`

is off by default, which leads to the following behavior:rlsimpl(a<>0 and (a>=0 or b=0)); => a <> 0 and (a > 0 or b = 0)This meets the simplification goal of small satisfaction sets for the atomic formulas. Turning on

`rlsipw`

will instead yield the following:rlsimpl(a<>0 and (a>0 or b=0)); => a <> 0 and (a >= 0 or b = 0)

Here we meet the simplification goal of convenient relations when strict orderings are considered inconvenient.

**rlsipo**

Simplification prefer orderings. Prefers orderings in contrast to inequalities with implicit theory simplification.

`rlsipo`

is on by default, which leads to the following behavior:rlsimpl(a>=0 and (a<>0 or b=0)); => a >= 0 and (a > 0 or b = 0)This meets the simplification goal of small satisfaction sets for the atomic formulas. Turning it on leads, e.g., to the following behavior:

rlsimpl(a>=0 and (a>0 or b=0)); => a >= 0 and (a <> 0 or b = 0)Here, we meet the simplification goal of convenient relations when orderings are considered inconvenient.

**rlsiatadv**

Simplify atomic formulas advanced. By default this switch is on. Enables sophisticated atomic formula simplifications based on squarefree part computations and recognition of trivial square sums.

rlsimpl(a**2 + 2*a*b + b**2 <> 0); => a+b <> 0 rlsimpl(a**2 + b**2 + 1 > 0); => trueFurthermore, splitting of trivial square sums (switch

`rlsitsqspl`

), parity decompositions (switch`rlsipd`

), and factorization of equations and inequalities (switch`rlsifac`

) are enabled.

**rlsitsqspl**

Simplify split trivial square sum. This is on by default. It is ignored with

`rlsiadv`

off. Trivial square sums are split additively depending on`rlsiexpl`

and`rlsiexpla`

(see General Standard Simplifier Switches):rlsimpl(a**2+b**2>0); => a <> 0 or b <> 0

**rlsipd**

Simplify parity decomposition. By default this switch is on. It is ignored with

`rlsiatadv`

off.`rlsipd`

toggles the parity decomposition of terms occurring with ordering relations.f := (a - 1)**3 * (a + 1)**4 >= 0; 7 6 5 4 3 2 => a + a - 3*a - 3*a + 3*a + 3*a - a - 1 >= 0 rlsimpl f; 3 2 => a + a - a - 1 >= 0The atomic formula is possibly split into two parts according to the setting of the switches

`rlsiexpl`

and`rlsiexpla`

(see General Standard Simplifier Switches).

**rlsifac**

Simplify factorization. By default this switch is on. It is ignored with

`rlsiatadv`

off. Splits equations and inequalities via factorization of their left hand side terms into a disjunction or a conjunction, respectively. This is done in dependence on`rlsiexpl`

and`rlsiexpla`

(see General Standard Simplifier Switches).

Next: ACFSF-specific Standard Simplifier Switches, Previous: OFSF-specific Standard Simplifier Switches, Up: Standard Simplifier

#### 4.1.5 ACFSF-specific Simplifications

In the acfsf case the atomic formula simplification includes the following:

- Evaluation of variable-free atomic formulas to truth values.
- Make the left hand sides primitive over the integers with positive head coefficient.
- Replace left hand sides of atomic formulas by their squarefree parts
(switch
`rlsiatdv`

, see OFSF-specific Standard Simplifier Switches). Optionally, perform factorization of equations and inequalities (switch`rlsifac`

, see OFSF-specific Standard Simplifier Switches, switches`rlsiexpl`

and`rlsiexpla`

, see General Standard Simplifier Switches).

For details see the description of the simplification for ordered fields in [DS97]. This can be easily adapted to algebraically closed fields.

Next: DVFSF-specific Simplifications, Previous: ACFSF-specific Simplifications, Up: Standard Simplifier

#### 4.1.6 ACFSF-specific Standard Simplifier Switches

The switches `rlsiatadv`

and `rlsifac`

have the same effects as in the ofsf
context (see OFSF-specific Standard Simplifier Switches).

Next: DVFSF-specific Standard Simplifier Switches, Previous: ACFSF-specific Standard Simplifier Switches, Up: Standard Simplifier

#### 4.1.7 DVFSF-specific Simplifications

In the dvfsf case the atomic formula simplification includes the following:

- Evaluation of variable-free atomic formulas to truth values provided that p is known.
- Equations and inequalities can be treated as in acfsf (see ACFSF-specific Simplifications). Moreover powers of p can be cancelled.
- With valuation relations, the gcd of both sides is cancelled and added appropriately as an equation or inequality.
- Valuation relations involving zero sides can be evaluated or at least turned into equations or inequalities.
- For concrete p, integer coefficients with valuation relations can be replaced by a power of p on one side of the relation.
- For unspecified p, polynomials in p can often be replaced by one monomial.
- For unspecified p, valuation relations containing a monomial in p on one
side, and an integer on the other side can be transformed into
`z ~ 1`

or`z /~ 1`

, where`z`

is an integer.

For details on simplification in p-adic fields see the article [DS99].

Atomic formulas of the form `z ~ 1`

or `z /~ 1`

, where
`z`

is an integer, can be split
into several ones via integer factorization.
This simplification is
often reasonable on final results. It explicitly discovers those primes
p for which the formula holds. There is a special function for this
simplification:

**rlexplats**

`formula`

Explode atomic formulas. Factorize atomic formulas of the form

`z ~ 1`

or`z /~ 1`

, where`z`

is an integer.`rlexplats`

obeys the switches`rlsiexpla`

and`rlsiexpl`

(see General Standard Simplifier Switches), but not`rlsifac`

(see DVFSF-specific Standard Simplifier Switches).

Next: PASF-specific Simplifications, Previous: DVFSF-specific Simplifications, Up: Standard Simplifier

#### 4.1.8 DVFSF-specific Standard Simplifier Switches

The context dvfsf
knows no special simplifier switches, and ignores the general switches
`rlsiexpla`

and `rlsiexpl`

(see General Standard Simplifier Switches). It behaves like
`rlsiexpla`

on. The simplifier contains numerous sophisticated
simplifications for atomic formulas in the style of `rlsiatadv`

on (see OFSF-specific Standard Simplifier Switches).

**rlsifac**

Simplify factorization. By default this switch is on. Toggles certain simplifications that require

integerfactorization. See DVFSF-specific Simplifications, for details.

Next: PASF-specific Standard Simplifier Switches, Previous: DVFSF-specific Standard Simplifier Switches, Up: Standard Simplifier

#### 4.1.9 PASF-specific Simplifications

Due to a simple term structure a lot simplification can be performed on pasf atomic formulas with the total goal of reducing the absolute summ of the coefficients. In the pasf context the atomic formula simplification includes the following:

- Evaluation of trivial domain valued atomic
formulas to truth values (e.g. variable free atomic formulas).
A special case of this simplification feature is the evaluation
of congruences with modulus equal to 1.
f := cong(y+x+z,0,1); rlsimpl f; => true

- Modulo reduction. The coefficients of a pasf
(in-)congurence modulo
m
can be reduced to be not greater than
m-1
After the application of this simplification rule
all coefficients could vanish to zero.
f := cong(7*x+5*y,11,3); rlsimpl f; => x + 2*y - 2 ~3~ 0 f := cong(8*x + 4*y, 16, 4); rlsimpl f; => true

- Content elimination in atomic formulas. Every atomic
(un-)equation can be done content free by dividing all
the coefficients by their greatest common divisor. Similar
simplification rule can be applied for the congruences.
In case of inequalities even more simplification can be done.
f := 3 * x + 6 * y - 9 = 0 rlsimpl f; => x + 2 * y - 3 = 0 f := 3 * x + 6 * y - 7 < 0 rlsimpl f; => x + 2 * y - 2 <= 0 f := cong(3 * x + 6 * y - 3, 0, 9); rlsimpl f; => x + 2 * y - 1 =~ 0 (3)

- In certain cases, we can simplify (un-)equations
and (in-)congruences to truth values. These simplification
rules due to their non-triviality are referred to as
the advanced simplification rules.
f := 3*k-1 = 0; rlsimpl f; => false

- pasf provides a simplification procedure for bounds using their special properties.
- Bounds that can't be satisfied, bounds with single satisfaction value and bounds with trivial matrix are transformed into equivalent unbounded formulas reducing the total formula length.
- Suitable atomic formulas in the matrix of a bounded quantifier that contain the bounded variable are moved inside the bound.
- Information from the bound is used to expand the implicit theory for the matrix simplification.

#### 4.1.10 PASF-specific Standard Simplifier Switches

**rlpasfsimplify**

Simplifies the output formula after the elimination of each quantifier. By default this switch is on.

**rlpasfexpand**

Expands the output formula (with bounded quantifiers) after the elimination of each quantifier. This switch is off by default due to immense overhead of the expansion.

**rlsiatadv**

Turns the advanced PASF-speciefic simplification of atomic formulas on. For details see See PASF-specific Simplifications.

Beside the standard simplification pasf provides a powerfull standard simplifier extension based on the package susi. This feature uses special properties of pasf formulas to reduce the formula size using the concept of implicit theory.

### 4.2 Tableau Simplifier

Although our standard simplifier (see Standard Simplifier) already combines information located on different boolean levels, it preserves the basic boolean structure of the formula. The tableau methods, in contrast, provide a technique for changing the boolean structure of a formula by constructing case distinctions. Compared to the standard simplifier they are much slower. For details on tableau simplification see [DS97].

**cdl**

Case distinction list. This is a list of atomic formulas considered as a disjunction.

**rltab**

`formula cdl`

Tableau method. The result is a tableau wrt.

cdl, i.e., a simplified equivalent of the disjunction over the specializations wrt. all atomic formulas incdl.rltab((a = 0 and (b = 0 or (d = 0 and e = 0))) or (a = 0 and c = 0),{a=0,a<>0}); => (a = 0 and (b = 0 or c = 0 or (d = 0 and e = 0)))

**rlatab**

`formula`

Automatic tableau method. Tableau steps wrt. a case distinction over the signs of all terms occurring in

formulaare computed and the best result, i.e., the result with the minimal number of atomic formulas is returned.

**rlitab**

`formula`

Iterative automatic tableau method.

formulais simplified by iterative applications of`rlatab`

. The exact procedure depends on the switch`rltabib`

.

**rltabib**

Tableau iterate branch-wise. By default this switch is on. It controls the procedure

`rlitab`

. If`rltabib`

is off,`rlatab`

is iteratively applied to the argument formula as long as shorter results can be obtained. In case`rltabib`

is on, the corresponding next tableau step is not applied to the last tableau result but independently to each single branch. The iteration stops when the obtained formula is not smaller than the corresponding input.

### 4.3 Groebner Simplifier

The Groebner simplifier is not available in the dvfsf context. It considers order theoretical and algebraic simplification rules between the atomic formulas of the input formula. Currently the Groebner simplifier is not idempotent. The name is derived from the main mathematical tool used for simplification: Computing Groebner bases of certain subsets of terms occurring in the atomic formulas.

For calling the Groebner simplifier there are the following functions:

**rlgsc**

`formula`[

`theory`]

— Function:

**rlgsd**

`formula`[

`theory`]

— Function:

**rlgsn**

`formula`[

`theory`]

Groebner simplifier.

formulais a quantifier-free formula. Default fortheoryis the empty theory`{}`

. The functions differ in the boolean normal form that is computed at the beginning.`rlgsc`

computes a conjunctive normal form,`rlgsd`

computes a disjunctive normal form, and`rlgsn`

heuristically decides for either a conjunctive or a disjunctive normal form depending on the structure offormula. After computing the corresponding normal form, the formula is simplified using Groebner simplification techniques. The returned formula is equivalent to the input formula wrt.theory.rlgsd(x=0 and ((y = 0 and x**2+2*y > 0) or (z=0 and x**3+z >= 0))); => x = 0 and z = 0rlgsc(x neq 0 or ((y neq 0 or x**2+2*x*y <= 0) and (z neq 0 or x**3+z < 0))); => x <> 0 or z <> 0

The heuristic used by `rlgsn`

is intended to find the smaller boolean normal form
among cnf an dnf. Note that, anyway, the simplification of the
smaller normal form can lead to a larger final result than that of the
larger one.

The Groebner simplifiers use the Groebner package of reduce to
compute the various Groebner bases. By default, the `revgradlex`

term order is used, and no optimizations of the order between the
variables are applied. The other switches and variables of the Groebner
package are not controlled by the Groebner simplifier. They can be
adjusted by the user.

In contrast to the standard simplifier `rlsimpl`

(see Standard Simplifier), the Groebner simplifiers can in general
produce formulas containing more atomic formulas than the input. This
cannot happen if the switches `rlgsprod`

,
`rlgsred`

,
and `rlgssub`

are off and the input formula is a simplified boolean normal form.

The functionality of the Groebner simplifiers `rlgsc`

,
`rlgsd`

,
and `rlgsn`

is controlled by numerous switches. In
most cases the default settings lead to a good simplification.

**rlgsrad**

Groebner simplifier radical membership test. By default this switch is on. If the switch is on the Groebner simplifier does not only use ideal membership tests for simplification but also radical membership tests. This leads to better simplifications but takes considerably more time.

**rlgssub**

Groebner simplifier substitute. By default this switch is on. Certain subsets of atomic formulas are substituted by equivalent ones. Both the number of atomic formulas and the complexity of the terms may increase or decrease independently.

**rlgsbnf**

Groebner simplifier boolean normal form. By default this switch is on. Then the simplification starts with a boolean normal form computation. If the switch is off, the simplifiers expect a boolean normal form as the argument

formula.

**rlgsred**

Groebner simplifier reduce polynomials. By default this switch is on. It controls the reduction of the terms wrt. the computed Groebner bases. The number of atomic formulas is never increased. Mind that by reduction the terms can become more complicated.

**rlgsvb**

Groebner simplifier verbose. By default this switch is on. It toggles verbosity output of the Groebner simplifier. Verbosity output is given if and only if both

`rlverbose`

(see Global Switches) and`rlgsvb`

are on.

**rlgsprod**

Groebner simplifier product. By default this switch is off. If this switch is on then conjunctions of inequalities and disjunctions of equations are contracted multiplicatively to one atomic formula. This reduces the number of atomic formulas but in most cases it raises the complexity of the terms. Most simplifications recognized by considering products are detected also with

`rlgsprod`

off.

**rlgserf**

Groebner simplifier evaluate reduced form. By default this switch is on. It controls the evaluation of the atomic formulas to truth values. If this switch is on, the standard simplifier (see Standard Simplifier) is used to evaluate atomic formulas. Otherwise atomic formulas are evaluated only if their left hand side is a domain element.

**rlgsutord**

Groebner simplifier user defined term order. By default this switch is off. Then all Groebner basis computations and reductions are performed with respect to the

`revgradlex`

term order. If this switch is on, the Groebner simplifier minds the term order selected with the`torder`

statement. For passing a variable list to`torder`

, note that`rlgsradmemv!*`

is used as the tag variable for radical membership tests.

**rlgsradmemv!***

Radical membership test variable. This fluid contains the tag variable used for the radical membership test with switch

`rlgsrad`

on. It can be used to pass the variable explicitly to`torder`

with switch`rlgsutord`

on.

### 4.4 Degree Decreaser

The quantifier elimination procedures of redlog (see Quantifier Elimination) obey certain degree restrictions on the bound variables. For this reason, there are degree-decreasing simplifiers available, which are automatically applied by the corresponding quantifier elimination procedures. There is no degree decreaser for the dvfsf context available.

**rldecdeg**

`formula`

Decrease degrees. Returns a formula equivalent to

formula, hopefully decreasing the degrees of the bound variables. In the ofsf context there are in general some sign conditions on the variables added, which slightly increases the number of contained atomic formulas.rldecdeg ex({b,x},m*x**4711+b**8>0); => ex b (b >= 0 and ex x (b + m*x > 0))

**rldecdeg1**

`formula`[

`varlist`]

Decrease degrees subroutine. This provides a low-level entry point to the degree decreaser. The variables to be decreased are not determined by regarding quantifiers but are explicitly given by

varlist, where the emptyvarlistselectsallfree variables of`f`

. The return value is a list`{f,l}`

.`f`

is a formula, and`l`

is a list`{...,{v,d},...}`

, where`v`

is fromvarlistand`d`

is an integer.`f`

has been obtained fromformulaby substituting`v`

for`v**d`

. The sign conditions necessary with the ofsf context are not generated automatically, but have to be constructed by hand for the variables`v`

with even degree`d`

in`l`

.rldecdeg1(m*x**4711+b**8>0,{b,x}); => {b + m*x > 0,{{x,4711},{b,8}}}

## 5 Normal Forms

### 5.1 Boolean Normal Forms

For computing small boolean normal forms,
see also the documentation of
the procedures `rlgsc`

and `rlgsd`

(Groebner Simplifier).

**rlcnf**

`formula`

Conjunctive normal form.

formulais a quantifier-free formula. Returns a conjunctive normal form offormula.rlcnf(a = 0 and b = 0 or b = 0 and c = 0); => (a = 0 or c = 0) and b = 0

**rldnf**

`formula`

Disjunctive normal form.

formulais a quantifier-free formula. Returns a disjunctive normal form offormula.rldnf((a = 0 or b = 0) and (b = 0 or c = 0)); => (a = 0 and c = 0) or b = 0

**rlbnfsm**

Boolean normal form smart. By default this switch is off. If on,

simplifier recognized implication(see [DS97]) is applied by`rlcnf`

and`rldnf`

. This leads to smaller normal forms but is considerably time consuming.

**rlbnfsac**

Boolean normal forms subsumption and cut. By default this switch is on. With boolean normal form computation, subsumption and cut strategies are applied by

`rlcnf`

and`rldnf`

to decrease the number of clauses. We give an example:rldnf(x=0 and y<0 or x=0 and y>0 or x=0 and y<>0 and z=0); => (x = 0 and y <> 0)

### 5.2 Miscellaneous Normal Forms

**rlnnf**

`formula`

Negation normal form. Returns a negation normal form of

formula. This is an`and`

-`or`

-combination of atomic formulas. Note that in all contexts, we use languages such that all negations can be encoded by relations (see Format and Handling of Formulas). We give an example:rlnnf(a = 0 equiv b > 0); => (a = 0 and b > 0) or (a <> 0 and b <= 0)

`rlnnf`

accepts formulas containing quantifiers, but it does not eliminate quantifiers.

**rlpnf**

`formula`

Prenex normal form. Returns a prenex normal form of

formula. The number of quantifier changes in the result is minimal among all prenex normal forms that can be obtained fromformulaby only moving quantifiers to the outside.When

formulacontains two quantifiers with the same variable such as inex x (x = 0) and ex x (x <> 0)there occurs a name conflict. It is resolved according to the following rules:

- Every bound variable that stands in conflict with any other variable is renamed.
- Free variables are never renamed.
Hence

`rlpnf`

applied to the above example formula yieldsrlpnf(ex(x,x=0) and ex(x,x<>0)); => ex x0 ex x1 (x0 = 0 and x1 <> 0)

**rlapnf**

`formula`

Anti-prenex normal form. Returns a formula equivalent to

formulawhere all quantifiers are moved to the inside as far as possible.rlapnf ex(x,all(y,x=0 or (y=0 and x=z))); => ex x (x = 0) or (all y (y = 0) and ex x (x - z = 0))

**rltnf**

`formula terml`

Term normal form.

termlis a list of terms. This combines dnf computation with tableau ideas (see Tableau Simplifier). A typical choice fortermlis`rlterml`

formula. If the switch`rltnft`

is off, then`rltnf(`

formula`,rlterml`

formula`)`

returns a dnf.

**rltnft**

Term normal form tree variant. By default this switch is on causing

`rltnf`

to return a deeply nested formula.

## 6 Quantifier Elimination and Variants

*Quantifier elimination* computes quantifier-free equivalents
for given first-order formulas.

For ofsf there are two methods available:

- Virtual substitution based on elimination set ideas [Wei88]. This implementation is restricted to at most quadratic occurrences of the quantified variables, but includes numerous heuristic strategies for coping with higher degrees. See [LW93], [Wei97], for details of the method.
- Partial cylindrical algebraic decomposition (CAD) introduced by Collins and Hong [CH91]. There are no degree restrictions with CAD.

For dvfsf we use the virtual substitution method that is also available for ofsf. Here, the implementation is restricted to linear occurrences of the quantified variables. There are also heuristic strategies for coping with higher degrees included. The method is described in detail in [Stu00].

The acfsf
quantifier elimination is based on *comprehensive
Groebner basis*
computation; there are no degree restrictions
for this context
[Wei92].

In pasf context the quantifier elimination is based on the fast method similar to elimination by virtual substitution introduced by Weispfenning. For more details see [Wei90]

### 6.1 Quantifier Elimination

#### 6.1.1 Virtual Substitution

**rlqe**

`formula`[

`theory`]

Quantifier elimination by virtual substitution. Returns a quantifier-free equivalent of

formula(wrt.theory). In the contexts ofsf and dvfsf,formulahas to obey certain degree restrictions. There are various techniques for decreasing the degree of the input and of intermediate results built in. In case that not all variables can be eliminated, the resulting formula is not quantifier-free but still equivalent.

For degree decreasing
heuristics see, e.g., Degree Decreaser, or the switches
`rlqeqsc`

/`rlqesqsc`

.

**elimination_answer**

A list of condition–solution pairs, i.e., a list of pairs consisting of a quantifier-free formula and a set of equations.

**rlqea**

`formula`[

`theory`]

Quantifier elimination with answer. Returns an

elimination_answerobtained the following way:formulais wlog. prenex. All quantifier blocks but the outermost one are eliminated. For this outermost block, the constructive information obtained by the elimination is saved:

- In case the considered block is existential, for each evaluation of the free variables we know the following: Whenever a condition holds, then
formulais`true`

under the given evaluation, and the solution isonepossible evaluation for the outer block variables satisfying the matrix.- The universally quantified case is dual: Whenever a condition is false, then
formulais`false`

, and the solution isonepossible counterexample.As an example we show how to find conditions and solutions for a system of two linear constraints:

rlqea ex(x,x+b1>=0 and a2*x+b2<=0); 2 - b2 => {{a2 *b1 - a2*b2 >= 0 and a2 <> 0,{x = -------}}, a2 {a2 < 0 or (a2 = 0 and b2 <= 0),{x = infinity1}}}The answer can contain constants named

`infinity`

or`epsilon`

, both indexed by a number: All`infinity`

's are positive and infinite, and all`epsilon`

's are positive and infinitesimal wrt. the considered field. Nothing is known about the ordering among the`infinity`

's and`epsilon`

's though this can be relevant for the points to be solutions. With the switch`rounded`

on, the`epsilon`

's are evaluated to zero.`rlqea`

is not available in the context acfsf.

**rlqeqsc**

— Switch:

**rlqesqsc**

Quantifier elimination (super) quadratic special case. By default these switches are off. They are relevant only in ofsf. If turned on, alternative elimination sets are used for certain special cases by

`rlqe`

/`rlqea`

and`rlgqe`

/`rlgqea`

. (see Generic Quantifier Elimination). They will possibly avoid violations of the degree restrictions, but lead to larger results in general. Former versions of redlog without these switches behaved as if`rlqeqsc`

was on and`rlqesqsc`

was off.

**rlqedfs**

Quantifier elimination depth first search. By default this switch is off. It is also ignored in the acfsf context. It is ignored with the switch

`rlqeheu`

on, which is the default for ofsf. Turning`rlqedfs`

on makes`rlqe`

/`rlqea`

and`rlgqe`

/`rlgqea`

(see Generic Quantifier Elimination) work in a depth first search manner instead of breadth first search. This saves space, and with decision problems, where variable-free atomic formulas can be evaluated to truth values, it might save time. In general, it leads to larger results.

**rlqeheu**

Quantifier elimination search heuristic. By default this switch is on in ofsf and off in dvfsf. It is ignored in acfsf. Turning

`rlqeheu`

on causes the switch`rlqedfs`

to be ignored.`rlqe`

/`rlqea`

and`rlgqe`

/`rlgqea`

(see Generic Quantifier Elimination) will then decide between breadth first search and depth first search for each quantifier block, where dfs is chosen when the problem is a decision problem.

**rlqepnf**

Quantifier elimination compute prenex normal form. By default this switch is on, which causes that

`rlpnf`

(see Miscellaneous Normal Forms) is applied toformulabefore starting the elimination process. If the argument formula to`rlqe`

/`rlqea`

or`rlgqe`

/`rlgqea`

(see Generic Quantifier Elimination) is already prenex, this switch can be turned off. This may be useful with formulas containing`equiv`

since`rlpnf`

applies`rlnnf`

, (see Miscellaneous Normal Forms), and resolving equivalences can double the size of a formula.`rlqepnf`

is ignored in acfsf, since nnf is necessary for elimination there.

**rlqesr**

Quantifier elimination separate roots. This is off by default. It is relevant only in ofsf for

`rlqe`

/`rlgqe`

and for all but the outermost quantifier block in`rlqea`

/`rlgqea`

. For`rlqea`

and`rlgqea`

see Generic Quantifier Elimination. It affects the technique for substituting the two solutions of a quadratic constraint during elimination.

The following two functions `rlqeipo`

and `rlqews`

are experimental implementations. The idea there is to overcome the
obvious disadvantages of prenex normal forms with elimination set
methods. In most cases, however, the classical method `rlqe`

has turned out superior.

**rlqeipo**

`formula`[

`theory`]

Quantifier elimination by virtual substitution in position. Returns a quantifier-free equivalent to

formulaby iteratively makingformulaanti-prenex (see Miscellaneous Normal Forms) and eliminating one quantifier.

**rlqews**

`formula`[

`theory`]

Quantifier elimination by virtual substitution with selection.

formulahas to be prenex, if the switch`rlqepnf`

is off. Returns a quantifier-free equivalent toformulaby iteratively selecting a quantifier from the innermost block, moving it inside as far as possible, and then eliminating it.`rlqews`

is not available in acfsf.

#### 6.1.2 Cylindrical Algebraic Decomposition

**rlcad**

`formula`

Cylindrical algebraic decomposition. Returns a quantifier-free equivalent of

formula. Works only in context OFSF. There are no degree restrictions onformula.

**rlcadporder**

`formula`

Efficient projection order. Returns a list of variables. The first variable is eliminated first.

**rlcadguessauto**

`formula`

Guess the size of a full CAD wrt. the projection order the system would actually choose. The resulting value gives quickly an idea on how big the order of magnitude of the size of a full CAD is.

**rlcadte**

Trial evaluation, the first improvement to partial CAD. This is turned on by default.

**rlcadpbfvs**

Propagation below free variable space, the second improvement to partial CAD. This is turned on by default.

**rlcadfulldimonly**

Full dimensional cells only. This is turned off by default. Only stacks over full dimensional cells are built. Such cells have rational sample points. To do this ist sound only in special cases as consistency problems (existenially quantified, strict inequalities).

**rlcadtrimtree**

Trim tree. This is turned on by default. Frees unused part of the constructed partial CAD-tree, and hence saves space. However, afterwards it is not possible anymore to find out how many cells were calculated beyond free variable space.

**rlcadrawformula**

Raw formula. Turned off by default. If turned on, a variable-free DNF is returned (if simple solution formula construction succeeds). Otherwise, the raw result is simplified with

`rldnf`

.

**rlcadisoallroots**

Isolate all roots. This is off by default. Turning this switch on allows to find out, how much time is consumed more without incremental root isolation.

**rlcadrawformula**

Raw formula. Turned off by default. If turned on, a variable-free DNF is returned (if simple solution formula construction succeeds). Otherwise, the raw result is simplified with

`rldnf`

.

**rlcadisoallroots**

Isolate all roots. This is off by default. Turning this switch on allows to find out, how much time is consumed more without incremental root isolation.

**rlcadaproj**

— Advanced Switch:

**rlcadaprojalways**

Augmented projection (always). By default,

`rlcadaproj`

is turned on and`rlcadaprojalways`

is turned off. If`rlcadaproj`

is turned off, no augmented projection is performed. Otherwerwise, if turned on, augmented projection is performed always (if`rlcadaprojalways`

is turned on) or just for the free variable space (`rlcadaprojalways`

turned off).

**rlcadhongproj**

Hong projection. This is on by default. If turned on, Hong's improvement for the projection operator is used.

**rlcadverbose**

Verbose. This is off by default. With

`rladverbose`

on, additional verbose information is displayed.

**rlcaddebug**

Debug. This is turned off by default. Performes a self-test at several places, if turned on.

**rlanuexverbose**

Verbose. This is off by default. With

`ranuexverbose`

on, additional verbose information is displayed. Not of much importance any more.

**rlanuexdifferentroots**

Different roots. Unused for the moment and maybe redundant soon.

**rlanuexdebug**

Debug. This is off by default. Performes a self-test at several places, if turned on.

**rlanuexpsremseq**

Pseudo remainder sequences. This is turned off by default. This switch decides, whether division or pseudo division is used for sturm chains.

**rlanuexgcdnormalize**

GCD normalize. This is turned on by default. If turned on, the GCD is normalized to 1, if it is a constant polynomial.

**rlanuexsgnopt**

Sign optimization. This is turned off by default. If turned on, it is tried to determine the sign of a constant polynomial by calculating a containment.

#### 6.1.3 Hermitian Quantifier Elimination

**rlhqe**

`formula`

Hermitian quantifier elimination. Returns a quantifier-free equivalent of

formula. Works only in context ofsf. There are no degree restrictions onformula.

Next: Local Quantifier Elimination, Previous: Quantifier Elimination, Up: Quantifier Elimination and Variants

### 6.2 Generic Quantifier Elimination

The following variant of `rlqe`

(see Quantifier Elimination) enlarges the theory by inequalities,
i.e., `<>`

-atomic formulas, wherever this supports the quantifier
elimination process. For geometric problems,
it has turned out that in most cases the additional assumptions made are
actually geometric *non-degeneracy conditions*.
The method has been described in detail in
[DSW98].
It has also turned out useful for physical problems
such as network
analysis, see [Stu97].

**rlgqe**

`formula`[

`theory`[

`exceptionlist`]]

Generic quantifier elimination.

`rlgqe`

is not available in acfsf and dvfsf.exceptionlistis a list of variables empty by default. Returns a list`{th,f}`

such that`th`

is a superset oftheoryadding only inequalities, and`f`

is a quantifier-free formula equivalent toformulaassuming`th`

. The added inequalities contain neither bound variables nor variables fromexceptionlist. For restrictions and options, compare`rlqe`

(see Quantifier Elimination).

**rlgqea**

`formula`[

`theory`[

`exceptionlist`]]

Generic quantifier elimination with answer.

`rlgqea`

is not available in acfsf and dvfsf.exceptionlistis a list of variables empty by default. Returns a list consisting of an extended theory and anelimination_answer. Compare`rlqea`

/`rlgqe`

(see Quantifier Elimination).

After applying generic quantifier elimination the user might feel that
the result is still too large while the theory is still quite weak. The
following function `rlgentheo`

simplifies a formula by making further assumptions.

**rlgentheo**

`theory formula`[

`exceptionlist`]

Generate theory.

`rlgentheo`

is not available in dvfsf.formulais a quantifier-free formula;exceptionlistis a list of variables empty by default.`rlgentheo`

extendstheorywith inequalities not containing any variables fromexceptionlistas long as the simplification result is better wrt. this extended theory. Returns a list`{`

extendedtheory, simplifiedformula`}`

.

**rlqegenct**

Quantifier elimination generate complex theory. This is on by default, which allows

`rlgentheo`

to assume inequalities over non-monomial terms with the generic quantifier elimination.

**rlgcad**

`formula`

Generic cylindrical algebraic decomposition.

`rlgcad`

is available only for ofsf. Compare`rlcad`

(see Quantifier Elimination) and`rlgqe`

(see Generic Quantifier Elimination).

**rlghqe**

`formula`

Generic Hermitian quantifier elimination.

`rlghqe`

is available only for ofsf. Compare`rlhqe`

(see Quantifier Elimination) and`rlgqe`

(see Generic Quantifier Elimination).

Next: Linear Optimization, Previous: Generic Quantifier Elimination, Up: Quantifier Elimination and Variants

### 6.3 Local Quantifier Elimination

In contrast to the generic quantifier elimination
(see Generic Quantifier Elimination)
the following variant of `rlqe`

(see Quantifier Elimination) enlarges the theory by arbitrary atomic formulas, wherever this supports the quantifier
elimination process. This is done in such a way that the theory holds
for the suggested point specified by the user.
The method has been described in detail in
[DW00].

**rllqe**

`formula theory suggestedpoint`

Local quantifier elimination.

`rllqe`

is not available in acfsf and dvfsf.suggestedpointis a list of equations`var=value`

where`var`

is a free variable and`value`

is a rational number. Returns a list`{th,f}`

such that`th`

is a superset oftheory, and`f`

is a quantifier-free formula equivalent toformulaassuming`th`

. The added inequalities contains exclusively variables occuring on the left hand sides of equiations insuggestedpoint. For restrictions and options, compare`rlqe`

(see Quantifier Elimination).

### 6.4 Linear Optimization

In the context ofsf, there is a linear optimization method implemented, which uses quantifier elimination (see Quantifier Elimination) encoding the target function by an additional constraint including a dummy variable. This optimization technique has been described in [Wei94a].

**rlopt**

`constraints target`

Linear optimization.

`rlopt`

is available only in ofsf.constraintsis a list of parameter-free atomic formulas built with`=`

,`<=`

, or`>=`

;targetis a polynomial over the rationals.targetis minimized subject toconstraints. The result is either "`infeasible`

" or a two-element list, the first entry of which is the optimal value, and the second entry is a list of points—each one given as asubstitution_list—wheretargettakes this value. The point list does, however, not contain all such points. For unbound problems the result is`{-infinity,{}}`

.

**rlopt1s**

Optimization one solution. This is off by default.

`rlopt1s`

is relevant only for ofsf. If on,`rlopt`

returns at most one solution point.

## 7 References

Most of the references listed here are available on

`http://www.fmi.uni-passau.de/~redlog/`.

- [CH91]
- George E. Collins and Hoon Hong. Partial cylindrical algebraic decomposition
for quantifier elimination. Journal of Symbolic
Computation, 12(3):299-328, September 1991.
- [Dol99]
- Andreas Dolzmann. Solving Geometric Problems with Real Quantifier
Elimination. Technical Report MIP-9903, FMI, Universitaet Passau,
D-94030 Passau, Germany, January 1999.
- [DGS98]
- Andreas Dolzmann, Oliver Gloor, and Thomas Sturm. Approaches to parallel
quantifier elimination. In Oliver Gloor, editor, Proceedings of
the 1998 International Symposium on Symbolic and Algebraic Computation
(ISSAC 98), pages 88-95, Rostock, Germany, August 1998. ACM, ACM Press,
New York.
- [DS97]
- Andreas Dolzmann and Thomas Sturm. Simplification of quantifier-free
formulae over ordered fields. Journal of Symbolic Computation,
24(2):209-231, August 1997.
- [DS97a]
- Andreas Dolzmann and Thomas Sturm. Redlog: Computer algebra meets computer
logic. ACM SIGSAM Bulletin, 31(2):2–9, June 1997.
- [DS97b]
- Andreas Dolzmann and Thomas Sturm. Guarded expressions in practice. In
Wolfgang W. Kuechlin, editor, Proceedings of the 1997
International Symposium on Symbolic and Algebraic Computation (ISSAC
97), pages 376–383, New York, July 1997. ACM, ACM Press.
- [DS99]
- Andreas Dolzmann and Thomas Sturm. P-adic constraint solving.
Technical Report MIP-9901, FMI, Universitaet Passau, D-94030
Passau, Germany, January 1999. To appear in the proceedings of the ISSAC
99.
- [DSW98]
- Andreas Dolzmann, Thomas Sturm, and Volker Weispfenning. A new approach
for automatic theorem proving in real geometry. Journal of
Automated Reasoning, 21(3):357-380, December 1998.
- [DSW98a]
- Andreas Dolzmann, Thomas Sturm, and Volker Weispfenning. Real quantifier
elimination in practice. In B. H. Matzat, G.-M. Greuel, and G. Hiss,
editors, Algorithmic Algebra and Number Theory, pages 221-248.
Springer, Berlin, 1998.
- [DW00]
- Andreas Dolzmann and Volker Weispfenning. Local Quantifier Elimination.
In Carlo Traverso, editor, Proceedings of the 2000 International
Symposium on Symbolic and Algebraic Computation (ISSAC 00), pages
86-94, St Andrews, Scotland, August 2000. ACM, ACM Press, New York.
- [LW93]
- Ruediger Loos and Volker Weispfenning. Applying linear quantifier
elimination. The Computer Journal, 36(5):450–462, 1993. Special
issue on computational quantifier elimination.
- [Stu97]
- Thomas Sturm. Reasoning over networks by symbolic methods. Technical
Report MIP-9719, FMI, Universitaet Passau, D-94030 Passau, Germany,
December 1997. To appear in AAECC.
- [Stu00]
- Thomas Sturm. Linear problems in valued fields. Journal of Symbolic
Computation, 30(2):207-219, August 2000.
- [SW97a]
- Thomas Sturm and Volker Weispfenning. Rounding and blending of solids by
a real elimination method. In Achim Sydow, editor, Proceedings of
the 15th IMACS World Congress on Scientific Computation, Modelling, and
Applied Mathematics (IMACS 97), pages 727-732, Berlin, August 1997.
IMACS, Wissenschaft & Technik Verlag.
- [SW98]
- Thomas Sturm and Volker Weispfenning. Computational geometry problems in
Redlog. In Dongming Wang, editor, Automated Deduction in
Geometry, volume 1360 of Lecture Notes in Artificial Intelligence
(Subseries of LNCS), pages 58-86, Springer-Verlag Berlin Heidelberg,
1998.
- [SW98a]
- Thomas Sturm and Volker Weispfenning. An algebraic approach to
offsetting and blending of solids. Technical Report MIP-9804, FMI,
Universitaet Passau, D-94030 Passau, Germany, May 1998.
- [Wei88]
- Volker Weispfenning. The complexity of linear problems in fields.
Journal of Symbolic Computation, 5(1):3–27, February, 1988.
- [Wei92]
- Volker Weispfenning. Comprehensive Groebner Bases.
Journal of Symbolic Computation, 14:1–29, July, 1992.
- [Wei94a]
- Volker Weispfenning. Parametric linear and quadratic optimization by
elimination. Technical Report MIP-9404, FMI, Universitaet Passau,
D-94030 Passau, Germany, April 1994.
- [Wei94b]
- Volker Weispfenning. Quantifier elimination for real algebra—the cubic
case. In Proceedings of the International Symposium on Symbolic
and Algebraic Computation in Oxford, pages 258–263, New York, July
1994. ACM Press.
- [Wei95]
- Volker Weispfenning. Solving parametric polynomial equations and
inequalities by symbolic algorithms. In J. Fleischer et al., editors,
Computer Algebra in Science and Engineering, pages 163-179, World
Scientific, Singapore, 1995.
- [Wei97]
- Volker Weispfenning. Quantifier elimination for real algebra—the
quadratic case and beyond. Applicable Algebra in Engineering
Communication and Computing, 8(2):85-101, February 1997.
- [Wei97a]
- Volker Weispfenning. Simulation and optimization by quantifier
elimination. Journal of Symbolic Computation, 24(2):189-208, August
1997.
- [Wei90]
- Volker Weispfenning. The complexity of almost linear diophantine problems. Journal of Symbolic Computation, 10(5):395-403, November 1990.

## Functions

### Documentation of Functions

`all`

: First-order Operators`and`

: First-order Operators`assoc`

: DVFSF Operators`ball`

: First-order Operators`band`

: IBALP Operators`bequiv`

: IBALP Operators`bex`

: First-order Operators`bimpl`

: IBALP Operators`bnot`

: IBALP Operators`bor`

: IBALP Operators`brepl`

: IBALP Operators`cong`

: PASF Operators`d`

: DCFSF Operators`div`

: DVFSF Operators`equal`

: PASF Operators`equal`

: DCFSF Operators`equal`

: IBALP Operators`equal`

: OFSF Operators`equal`

: DVFSF Operators`equal`

: ACFSF Operators`equiv`

: First-order Operators`ex`

: First-order Operators`for`

: Extended Built-in Commands`geq`

: OFSF Operators`geq`

: PASF Operators`greaterp`

: PASF Operators`greaterp`

: OFSF Operators`impl`

: First-order Operators`length`

: Extended Built-in Commands`leq`

: PASF Operators`leq`

: OFSF Operators`lessp`

: PASF Operators`lessp`

: OFSF Operators`mkand`

: Extended Built-in Commands`mkor`

: Extended Built-in Commands`nassoc`

: DVFSF Operators`ncong`

: PASF Operators`neq`

: ACFSF Operators`neq`

: PASF Operators`neq`

: DVFSF Operators`neq`

: OFSF Operators`neq`

: DCFSF Operators`not`

: First-order Operators`or`

: First-order Operators`part`

: Extended Built-in Commands`repl`

: First-order Operators`rlall`

: Closures`rlapnf`

: Miscellaneous Normal Forms`rlatab`

: Tableau Simplifier`rlatl`

: Basic Functions on Formulas`rlatml`

: Basic Functions on Formulas`rlatnum`

: Basic Functions on Formulas`rlbvarl`

: Basic Functions on Formulas`rlcad`

: Quantifier Elimination`rlcadguessauto`

: Quantifier Elimination`rlcadporder`

: Quantifier Elimination`rlcnf`

: Boolean Normal Forms`rldecdeg`

: Degree Decreaser`rldecdeg1`

: Degree Decreaser`rldnf`

: Boolean Normal Forms`rlex`

: Closures`rlexplats`

: DVFSF-specific Simplifications`rlfvarl`

: Basic Functions on Formulas`rlgcad`

: Generic Quantifier Elimination`rlgentheo`

: Generic Quantifier Elimination`rlghqe`

: Generic Quantifier Elimination`rlgqe`

: Generic Quantifier Elimination`rlgqea`

: Generic Quantifier Elimination`rlgsc`

: Groebner Simplifier`rlgsd`

: Groebner Simplifier`rlgsn`

: Groebner Simplifier`rlhqe`

: Quantifier Elimination`rlifacl`

: Basic Functions on Formulas`rlifacml`

: Basic Functions on Formulas`rlifstruct`

: Basic Functions on Formulas`rlitab`

: Tableau Simplifier`rllqe`

: Local Quantifier Elimination`rlmatrix`

: Basic Functions on Formulas`rlnnf`

: Miscellaneous Normal Forms`rlopt`

: Linear Optimization`rlpnf`

: Miscellaneous Normal Forms`rlqe`

: Quantifier Elimination`rlqea`

: Quantifier Elimination`rlqeipo`

: Quantifier Elimination`rlqews`

: Quantifier Elimination`rlset`

: Context Selection`rlsimpl`

: Standard Simplifier`rlstruct`

: Basic Functions on Formulas`rltab`

: Tableau Simplifier`rlterml`

: Basic Functions on Formulas`rltermml`

: Basic Functions on Formulas`rltnf`

: Miscellaneous Normal Forms`rlvarl`

: Basic Functions on Formulas`sdiv`

: DVFSF Operators`sub`

: Extended Built-in Commands

### References to Functions

`and`

: Extended Built-in Commands`equiv`

: Quantifier Elimination`for`

: First-order Operators`impl`

: General Features of the Standard Simplifier`load_package`

: Loading Redlog`not`

: General Features of the Standard Simplifier`or`

: Extended Built-in Commands`part`

: Extended Built-in Commands`part`

: Overview`repl`

: General Features of the Standard Simplifier`rlatab`

: Tableau Simplifier`rlcnf`

: Boolean Normal Forms`rldnf`

: Boolean Normal Forms`rlgentheo`

: Generic Quantifier Elimination`rlgqe`

: Quantifier Elimination`rlgqe`

: Local Quantifier Elimination`rlgqe`

: Quantifier Elimination`rlgqea`

: Quantifier Elimination`rlgsc`

: Groebner Simplifier`rlgsc`

: Boolean Normal Forms`rlgsd`

: Boolean Normal Forms`rlgsd`

: Groebner Simplifier`rlgsn`

: Groebner Simplifier`rlitab`

: Tableau Simplifier`rlmatrix`

: Extended Built-in Commands`rlnnf`

: Quantifier Elimination`rlopt`

: Linear Optimization`rlpnf`

: Quantifier Elimination`rlqe`

: Quantifier Elimination`rlqe`

: Context Selection`rlqe`

: Local Quantifier Elimination`rlqe`

: Generic Quantifier Elimination`rlqe`

: Quantifier Elimination`rlqea`

: Quantifier Elimination`rlqea`

: Context Selection`rlqea`

: Quantifier Elimination`rlqeipo`

: Quantifier Elimination`rlqews`

: Quantifier Elimination`rlset`

: Context Selection`rlsimpl`

: General Standard Simplifier Switches`rlsimpl`

: Groebner Simplifier`rlsimpl`

: PASF-specific Simplifications`rlsimpl`

: OFSF-specific Standard Simplifier Switches`rlsimpl`

: General Standard Simplifier Switches`rlsimpl`

: Global Switches`rlterml`

: Miscellaneous Normal Forms`sub`

: Extended Built-in Commands`sub`

: Overview`torder`

: Groebner Simplifier

## Switches and Variables

### Documentation of Switches and Variables

`false`

: First-order Operators`rladdcond`

: OFSF Operators`rlanuexdebug`

: Quantifier Elimination`rlanuexdifferentroots`

: Quantifier Elimination`rlanuexgcdnormalize`

: Quantifier Elimination`rlanuexpsremseq`

: Quantifier Elimination`rlanuexsgnopt`

: Quantifier Elimination`rlanuexverbose`

: Quantifier Elimination`rlbnfsac`

: Boolean Normal Forms`rlbnfsm`

: Boolean Normal Forms`rlbrop`

: First-order Operators`rlcadaproj`

: Quantifier Elimination`rlcadaprojalways`

: Quantifier Elimination`rlcadbaseonly`

: Quantifier Elimination`rlcaddebug`

: Quantifier Elimination`rlcadextonly`

: Quantifier Elimination`rlcadfac`

: Quantifier Elimination`rlcadfulldimonly`

: Quantifier Elimination`rlcadhongproj`

: Quantifier Elimination`rlcadisoallroots`

: Quantifier Elimination`rlcadpartial`

: Quantifier Elimination`rlcadpbfvs`

: Quantifier Elimination`rlcadprojonly`

: Quantifier Elimination`rlcadrawformula`

: Quantifier Elimination`rlcadte`

: Quantifier Elimination`rlcadtrimtree`

: Quantifier Elimination`rlcadverbose`

: Quantifier Elimination`RLDEFLANG`

: Context Selection`rldeflang!*`

: Context Selection`rlgsbnf`

: Groebner Simplifier`rlgserf`

: Groebner Simplifier`rlgsprod`

: Groebner Simplifier`rlgsrad`

: Groebner Simplifier`rlgsradmemv!*`

: Groebner Simplifier`rlgsred`

: Groebner Simplifier`rlgssub`

: Groebner Simplifier`rlgsutord`

: Groebner Simplifier`rlgsvb`

: Groebner Simplifier`rlnzden`

: OFSF Operators`rlopt1s`

: Linear Optimization`rlpasfexpand`

: PASF-specific Standard Simplifier Switches`rlpasfsimplify`

: PASF-specific Standard Simplifier Switches`rlposden`

: OFSF Operators`rlqedfs`

: Quantifier Elimination`rlqegenct`

: Generic Quantifier Elimination`rlqeheu`

: Quantifier Elimination`rlqepnf`

: Quantifier Elimination`rlqeqsc`

: Quantifier Elimination`rlqesqsc`

: Quantifier Elimination`rlqesr`

: Quantifier Elimination`rlrealtime`

: Global Switches`rlsiatadv`

: PASF-specific Standard Simplifier Switches`rlsiatadv`

: OFSF-specific Standard Simplifier Switches`rlsichk`

: General Standard Simplifier Switches`rlsiexpl`

: General Standard Simplifier Switches`rlsiexpla`

: General Standard Simplifier Switches`rlsifac`

: DVFSF-specific Standard Simplifier Switches`rlsifac`

: OFSF-specific Standard Simplifier Switches`rlsiidem`

: General Standard Simplifier Switches`rlsimpl`

: Global Switches`rlsipd`

: OFSF-specific Standard Simplifier Switches`rlsipo`

: OFSF-specific Standard Simplifier Switches`rlsipw`

: OFSF-specific Standard Simplifier Switches`rlsism`

: General Standard Simplifier Switches`rlsiso`

: General Standard Simplifier Switches`rlsitsqspl`

: OFSF-specific Standard Simplifier Switches`rlsusi`

: PASF-specific Standard Simplifier Switches`rltabib`

: Tableau Simplifier`rltnft`

: Miscellaneous Normal Forms- prefer orderings: OFSF-specific Standard Simplifier Switches
- prefer weak orderings: OFSF-specific Standard Simplifier Switches
- prenex normal form: Quantifier Elimination
- prenex normal form: Miscellaneous Normal Forms
- prenex normal form: Quantifier Elimination
- primitive over the integers: OFSF-specific Simplifications
- primitive over the integers: ACFSF-specific Simplifications
- projection order: Quantifier Elimination
- protocol: Groebner Simplifier
- protocol: Global Switches
- quadratic constraint: Quantifier Elimination
- quadratic special case: Quantifier Elimination
- quantifier: Closures
- quantifier: Miscellaneous Normal Forms
- quantifier: Basic Functions on Formulas
- quantifier: First-order Operators
- quantifier: Miscellaneous Normal Forms
- quantifier: Closures
- quantifier block: Quantifier Elimination
- quantifier changes: Miscellaneous Normal Forms
- quantifier elimination: Quantifier Elimination
- quantifier elimination: Linear Optimization
- quantifier elimination: Quantifier Elimination
- quantifier elimination: OFSF Operators
- quantifier-free equivalent: Quantifier Elimination and Variants
- quantifier-free equivalent: Quantifier Elimination
- radical membership test: Groebner Simplifier
- rational numbers: OFSF Operators
- real closed field: Contexts
- real closed field: OFSF Operators
- real closed field: Contexts
- real numbers: Contexts
- real time: Global Switches
- reciprocal: OFSF Operators
- reduce polynomials: Groebner Simplifier
- relations: Context Selection
- remove quantifiers: Basic Functions on Formulas
- rename variables: Miscellaneous Normal Forms
- replication: First-order Operators
`revgradlex`

: Groebner Simplifier- sample solution: Quantifier Elimination
- save space: Quantifier Elimination
- save time: Quantifier Elimination
- search heuristic: Quantifier Elimination
- separate roots: Quantifier Elimination
- set of atomic formulas: Basic Functions on Formulas
- set of irreducible factors: Basic Functions on Formulas
- set of variables: Basic Functions on Formulas
- sign conditions: Degree Decreaser
- simplification: General Standard Simplifier Switches
- simplification: Tableau Simplifier
- simplification: OFSF-specific Standard Simplifier Switches
- simplification: DVFSF-specific Standard Simplifier Switches
- simplification: Standard Simplifier
- simplification: Simplification
- simplification: Tableau Simplifier
- simplification: OFSF-specific Standard Simplifier Switches
- simplification: Tableau Simplifier
- simplification: General Standard Simplifier Switches
- simplification: Global Switches
- simplification: General Standard Simplifier Switches
- simplification: Generic Quantifier Elimination
- simplification: General Standard Simplifier Switches
- simplification: OFSF-specific Standard Simplifier Switches
- simplification: Groebner Simplifier
- simplification: OFSF-specific Standard Simplifier Switches
- simplification of atomic formulas: PASF-specific Simplifications
- simplification of atomic formulas: OFSF-specific Simplifications
- simplification of atomic formulas: ACFSF-specific Simplifications
- simplification of atomic formulas: DVFSF-specific Simplifications
- simplification of atomic formulas: OFSF-specific Standard Simplifier Switches
- simplifier recognized implication: Boolean Normal Forms
- small satisfaction sets: OFSF-specific Standard Simplifier Switches
- smart bnf computation: Boolean Normal Forms
- smart simplification: General Standard Simplifier Switches
- smart simplification: General Features of the Standard Simplifier
- solution: Linear Optimization
- solution: Quantifier Elimination
- solution points: Quantifier Elimination
- sort atomic formulas: General Standard Simplifier Switches
- split trivial square sum: OFSF-specific Standard Simplifier Switches
- split atomic formula: OFSF-specific Simplifications
- split atomic formula: OFSF-specific Standard Simplifier Switches
- split atomic formula: DVFSF-specific Simplifications
- split atomic formula: General Standard Simplifier Switches
- split atomic formula: DVFSF-specific Simplifications
- split trivial square sum: OFSF-specific Standard Simplifier Switches
- squarefree part: OFSF-specific Simplifications
- squarefree part: OFSF-specific Standard Simplifier Switches
- squarefree part: ACFSF-specific Simplifications
- standard simplifier: Groebner Simplifier
- standard simplifier: Standard Simplifier
- starting redlog: Loading and Context Selection
- strict divisibility: DVFSF Operators
- strict orderings: OFSF-specific Standard Simplifier Switches
- structure of formula: Basic Functions on Formulas
- substitution: Extended Built-in Commands
- substitution: Groebner Simplifier
- substitution: Degree Decreaser
- substitution: Basic Functions on Formulas
- substitution: Quantifier Elimination
- subsumption: Boolean Normal Forms
- super quadratic special case: Quantifier Elimination
- switch: Conventions
- tableau: Miscellaneous Normal Forms
- tableau: Tableau Simplifier
- tag variable: Groebner Simplifier
- term list: Basic Functions on Formulas
- term multiplicity list: Basic Functions on Formulas
- term normal form: Miscellaneous Normal Forms
- term order: Groebner Simplifier
- theory: Context Selection
- theory: Generic Quantifier Elimination
- theory (implicit): General Features of the Standard Simplifier
- time: Global Switches
- trivial square sum: OFSF-specific Simplifications
- trivial square sum: OFSF-specific Standard Simplifier Switches
- truth value: Groebner Simplifier
- truth value: First-order Operators
- truth value: General Features of the Standard Simplifier
- truth value: OFSF-specific Simplifications
- truth value: Basic Functions on Formulas
- truth value: Extended Built-in Commands
- truth value: ACFSF-specific Simplifications
- truth value: Quantifier Elimination
- truth value: DVFSF-specific Simplifications
- truth value: First-order Operators
- universal closure: Closures
- unsplit atomic formulas: Groebner Simplifier
- valuation (p-adic): Context Selection
- valuation relation: DVFSF-specific Simplifications
- valued field: Context Selection
- variable list(s): Basic Functions on Formulas
- variable renaming: Miscellaneous Normal Forms
- variable-free atomic formula: DVFSF-specific Simplifications
- variable-free atomic formula: ACFSF-specific Simplifications
- variable-free atomic formula: OFSF-specific Simplifications
- verbosity output: Global Switches
- verbosity output: Groebner Simplifier
- virtual substitution: Quantifier Elimination and Variants
- wall clock time: Global Switches
- weak divisibility: DVFSF Operators
- weak orderings: OFSF-specific Standard Simplifier Switches

## Short Contents

## Table of Contents

- Contents
- 1 Introduction
- 2 Loading and Context Selection
- 3 Format and Handling of Formulas
- 4 Simplification
- 4.1 Standard Simplifier
- 4.1.1 General Features of the Standard Simplifier
- 4.1.2 General Standard Simplifier Switches
- 4.1.3 OFSF-specific Simplifications
- 4.1.4 OFSF-specific Standard Simplifier Switches
- 4.1.5 ACFSF-specific Simplifications
- 4.1.6 ACFSF-specific Standard Simplifier Switches
- 4.1.7 DVFSF-specific Simplifications
- 4.1.8 DVFSF-specific Standard Simplifier Switches
- 4.1.9 PASF-specific Simplifications
- 4.1.10 PASF-specific Standard Simplifier Switches

- 4.2 Tableau Simplifier
- 4.3 Groebner Simplifier
- 4.4 Degree Decreaser

- 4.1 Standard Simplifier
- 5 Normal Forms
- 6 Quantifier Elimination and Variants
- 7 References
- Functions
- Switches and Variables
- Data Structures
- Index