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

— Function: rlset [context [arguments...]]
— Function: rlset argument-list

Set current context. Valid choices for context are 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 optional dvf_class_specification can 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.

— Data Structure: 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.

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

— Fluid: 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 loading redlog.

— Environment Variable: 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.

— Unary Operator: 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.

— 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.

— Binary Operator: 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.

— Binary Operator: 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.

— Variable: true
— Variable: false

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

— Function: rlall formula [exceptionlist]

Universal closure. exceptionlist is a list of variables empty by default. Returns formula with all free variables universally quantified, except for those in exceptionlist.

— Function: rlex formula [exceptionlist]

Existential closure. exceptionlist is a list of variables empty by default. Returns formula with all free variables existentially quantified, except for those in exceptionlist.

— Binary Infix operator: 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 input chains of 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 = 0
     

Here, only adjacent terms are related to each other.

— Switch: 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  > 0
     

Turning 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
     

— Switch: 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)
     

— Binary Infix operator: 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 of chains in analogy to ofsf. See OFSF Operators, for details.

— Binary Infix operator: 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 of chains and an appropriate treatment of parametric denominators in the input. See OFSF Operators, for details.

— Binary Infix operator: 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~ 0
     

As 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 chains See OFSF Operators, for details.

— Unary operator: 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.

— Binary Infix operator: equal

The operator equal may also be written as =.

— Binary Infix operator: d

The operator d denotes (higher) derivatives in the sense of differential algebra. For instance, the differential equation

          x'^2 + x = 0
     

is input as x d 1 ** 2 + x = 0. d binds stronger than all other operators.

— Binary Infix operator: equal
— Binary Infix operator: neq

The operator equal may also be written as =. The operator neq may also be written as <>.

— for loop action: 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)
     

— Data Structure: substitution_list

substitution_list is a list of equations each with a kernel left hand side.

— Function: sub substitution_list formula

Substitute. Returns the formula obtained from formula by applying the substitutions given by substitution_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.

— Function: part formula n1 [n2 [n3...]]

Extract a part. The part of formula is implemented analogously to that for built-in types: in particular the 0th part is the operator.

— Function: 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.

— Switch: rlsimpl

Simplify. By default this switch is off. With this switch on, the function rlsimpl is applied at the expression evaluation stage. See rlsimpl.

— Switch: 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 printed above the result.

— Advanced Switch: rlverbose

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

— Function: 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.

— Data Structure: multiplicity_list

A list of 2-element-lists containing an object and the number of its occurrences. Names of functions returning multiplicity_lists typically end on "ml".

— Function: rlatl formula

List of atomic formulas. Returns the set of atomic formulas contained in formula as a list.

— Function: rlatml formula

Multiplicity list of atomic formulas. Returns the atomic formulas contained in formula in a multiplicity_list.

— Function: 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}
     

— Function: rlifacml formula

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

— Function: rlterml formula

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

— Function: rltermml formula

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

— Function: rlvarl formula

Variable lists. Returns both the list of variables occurring freely and that of the variables occurring boundly in formula in a two-element list. Notice that the two member lists are not necessarily disjoint.

— Function: rlfvarl formula

Free variable list. Returns the variables occurring freely in formula as a list.

— Function: rlbvarl formula

Bound variable list. Returns the variables occurring boundly in formula as a list.

— Function: rlstruct formula [kernel]

Structure of a formula. kernel is v by default. Returns a list {f,sl}. f is constructed from formula by replacing each occurrence of a term with a kernel constructed by concatenating a number to kernel. The substitution_list sl contains all substitutions to obtain formula from 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}}
     

— Function: rlifstruct formula [kernel]

Irreducible factor structure of a formula. kernel is v by default. Returns a list {f,sl}. f is constructed from formula by replacing each occurrence of an irreducible factor with a kernel constructed by adding a number to kernel. The returned substitution_list sl contains all substitutions to obtain formula from 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}}
     

— Function: rlmatrix formula

Matrix computation. Drops all leading quantifiers from formula.

— Data Structure: theory

A list of atomic formulas assumed to hold.

— Function: rlsimpl formula [theory]

Simplify. formula is simplified recursively such that the result is equivalent under the assumption that theory holds. Default for theory is the empty theory {}. Theory inconsistency may but need not be detected by rlsimpl. If theory is detected to be inconsistent, a corresponding error is raised. Note that under an inconsistent theory, any formula is equivalent to the input, i.e., the result is meaningless. theory should thus be chosen carefully.

— Switch: 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 = 0
     

With 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.

— Switch: 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 on

            7    6      5      4      3      2
          a  + a  - 3*a  - 3*a  + 3*a  + 3*a  - a - 1 >= 0
     

simplifies 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.

— Fix Switch: 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
     

— Fix Switch: 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)
          

— Fix Switch: 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.

— Fix Switch: 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
     

— Switch: 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)
     

— Switch: 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.

— Switch: 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);
               => true
     

Furthermore, splitting of trivial square sums (switch rlsitsqspl), parity decompositions (switch rlsipd), and factorization of equations and inequalities (switch rlsifac) are enabled.

— Switch: 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
     

— Switch: 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 >= 0
     

The atomic formula is possibly split into two parts according to the setting of the switches rlsiexpl and rlsiexpla (see General Standard Simplifier Switches).

— Switch: 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).

— Function: 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).

— Switch: rlsifac

Simplify factorization. By default this switch is on. Toggles certain simplifications that require integer factorization. See DVFSF-specific Simplifications, for details.

— Switch: rlpasfsimplify

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

— Switch: 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.

— Switch: rlsiatadv

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

— Switch: rlsusi

Turns the advanced susi simplification on. Per default this switch is on.

— Data Structure: cdl

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

— Function: 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 in cdl.

          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)))
     

— Function: rlatab formula

Automatic tableau method. Tableau steps wrt. a case distinction over the signs of all terms occurring in formula are computed and the best result, i.e., the result with the minimal number of atomic formulas is returned.

— Function: rlitab formula

Iterative automatic tableau method. formula is simplified by iterative applications of rlatab. The exact procedure depends on the switch rltabib.

— Switch: 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.

— Function: rlgsc formula [theory]
— Function: rlgsd formula [theory]
— Function: rlgsn formula [theory]

Groebner simplifier. formula is a quantifier-free formula. Default for theory is 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 of formula. 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 = 0
     

          rlgsc(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
     

— Switch: 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.

— Switch: 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.

— Switch: 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.

— Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: 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.

— Fluid: 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.

— Function: 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))
     

— Function: 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 empty varlist selects all free 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 from varlist and d is an integer. f has been obtained from formula by 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}}}
     

— Function: rlcnf formula

Conjunctive normal form. formula is a quantifier-free formula. Returns a conjunctive normal form of formula.

          rlcnf(a = 0 and b = 0 or b = 0 and c = 0);
              => (a = 0 or c = 0) and b = 0
     

— Function: rldnf formula

Disjunctive normal form. formula is a quantifier-free formula. Returns a disjunctive normal form of formula.

          rldnf((a = 0 or b = 0) and (b = 0 or c = 0));
              => (a = 0 and c = 0) or b = 0
     

— Switch: 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.

— Fix Switch: 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)
     

— Function: 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.

— Function: 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 from formula by only moving quantifiers to the outside.

When formula contains two quantifiers with the same variable such as in

          ex 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 yields

          rlpnf(ex(x,x=0) and ex(x,x<>0));
              => ex x0 ex x1 (x0 = 0 and x1 <> 0)
     

— Function: rlapnf formula

Anti-prenex normal form. Returns a formula equivalent to formula where 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))
     

— Function: rltnf formula terml

Term normal form. terml is a list of terms. This combines dnf computation with tableau ideas (see Tableau Simplifier). A typical choice for terml is rlterml formula. If the switch rltnft is off, then rltnf(formula,rlterml formula) returns a dnf.

— Switch: rltnft

Term normal form tree variant. By default this switch is on causing rltnf to return a deeply nested formula.

— Function: rlqe formula [theory]

Quantifier elimination by virtual substitution. Returns a quantifier-free equivalent of formula (wrt. theory). In the contexts ofsf and dvfsf, formula has 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.

— Data Structure: 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.

— Function: rlqea formula [theory]

Quantifier elimination with answer. Returns an elimination_answer obtained the following way: formula is 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 formula is true under the given evaluation, and the solution is one possible evaluation for the outer block variables satisfying the matrix.
• The universally quantified case is dual: Whenever a condition is false, then formula is false, and the solution is one possible 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.

— Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: rlqepnf

Quantifier elimination compute prenex normal form. By default this switch is on, which causes that rlpnf (see Miscellaneous Normal Forms) is applied to formula before 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.

— Fix Switch: 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.

— Function: rlqeipo formula [theory]

Quantifier elimination by virtual substitution in position. Returns a quantifier-free equivalent to formula by iteratively making formula anti-prenex (see Miscellaneous Normal Forms) and eliminating one quantifier.

— Function: rlqews formula [theory]

Quantifier elimination by virtual substitution with selection. formula has to be prenex, if the switch rlqepnf is off. Returns a quantifier-free equivalent to formula by 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.

— Function: rlcad formula

Cylindrical algebraic decomposition. Returns a quantifier-free equivalent of formula. Works only in context OFSF. There are no degree restrictions on formula.

— Function: rlcadporder formula

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

— Function: 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.

— Advanced Switch: rlcadfac

Factorisation. This is on by default.

— Switch: rlcadbaseonly

Base phase only. Turned off by default.

— Switch: rlcadprojonly

Projection phase only. Turned off by default.

— Switch: rlcadextonly

Extension phase only. Turned off by default.

— Switch: rlcadpartial

Partial CAD. This is turned on by default.

— Switch: rlcadte

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

— Switch: rlcadpbfvs

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

— Advanced Switch: 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).

— Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: 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.

— Advanced Switch: 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).

— Switch: rlcadhongproj

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

— Switch: rlcadverbose

Verbose. This is off by default. With rladverbose on, additional verbose information is displayed.

— Switch: rlcaddebug

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

— Advanced Switch: rlanuexverbose

Verbose. This is off by default. With ranuexverbose on, additional verbose information is displayed. Not of much importance any more.

— Advanced Switch: rlanuexdifferentroots

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

— Switch: rlanuexdebug

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

— Switch: rlanuexpsremseq

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

— Advanced Switch: rlanuexgcdnormalize

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

— Advanced Switch: 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.

— Function: rlhqe formula

Hermitian quantifier elimination. Returns a quantifier-free equivalent of formula. Works only in context ofsf. There are no degree restrictions on formula.

— Function: rlgqe formula [theory [exceptionlist]]

Generic quantifier elimination. rlgqe is not available in acfsf and dvfsf. exceptionlist is a list of variables empty by default. Returns a list {th,f} such that th is a superset of theory adding only inequalities, and f is a quantifier-free formula equivalent to formula assuming th. The added inequalities contain neither bound variables nor variables from exceptionlist. For restrictions and options, compare rlqe (see Quantifier Elimination).

— Function: rlgqea formula [theory [exceptionlist]]

Generic quantifier elimination with answer. rlgqea is not available in acfsf and dvfsf. exceptionlist is a list of variables empty by default. Returns a list consisting of an extended theory and an elimination_answer. Compare rlqea/rlgqe (see Quantifier Elimination).

— Function: rlgentheo theory formula [exceptionlist]

Generate theory. rlgentheo is not available in dvfsf. formula is a quantifier-free formula; exceptionlist is a list of variables empty by default. rlgentheo extends theory with inequalities not containing any variables from exceptionlist as long as the simplification result is better wrt. this extended theory. Returns a list {extended theory, simplified formula}.

— Switch: 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.

— Function: rlgcad formula

Generic cylindrical algebraic decomposition. rlgcad is available only for ofsf. Compare rlcad (see Quantifier Elimination) and rlgqe (see Generic Quantifier Elimination).

— Function: rlghqe formula

Generic Hermitian quantifier elimination. rlghqe is available only for ofsf. Compare rlhqe (see Quantifier Elimination) and rlgqe (see Generic Quantifier Elimination).

— Function: rllqe formula theory suggestedpoint

Local quantifier elimination. rllqe is not available in acfsf and dvfsf. suggestedpoint is 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 of theory, and f is a quantifier-free formula equivalent to formula assuming th. The added inequalities contains exclusively variables occuring on the left hand sides of equiations in suggestedpoint. For restrictions and options, compare rlqe (see Quantifier Elimination).

— Function: rlopt constraints target

Linear optimization. rlopt is available only in ofsf. constraints is a list of parameter-free atomic formulas built with =, <=, or >=; target is a polynomial over the rationals. target is minimized subject to constraints. 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 a substitution_list—where target takes this value. The point list does, however, not contain all such points. For unbound problems the result is {-infinity,{}}.

— Switch: rlopt1s

Optimization one solution. This is off by default. rlopt1s is relevant only for ofsf. If on, rlopt returns at most one solution point.