Redlog Documentation

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.


Next: , Up: (dir)

Contents


Next: , Previous: Top, Up: Top

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.


Next: , Up: Introduction

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.


Next: , Previous: Contexts, Up: Introduction

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:


Previous: Overview, Up: Introduction

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.


Next: , Previous: Introduction, Up: Top

2 Loading and Context Selection


Next: , Up: 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.


Previous: Loading Redlog, Up: Loading and Context Selection

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:

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

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.

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

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.

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


Next: , Previous: Loading and Context Selection, Up: Top

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.


Next: , Up: Format and Handling of Formulas

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.

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

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

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

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

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

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

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

— Variable: true
— Variable: false

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


Next: , Previous: First-order Operators, Up: Format and Handling of Formulas

3.2 Closures

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


Next: , Previous: Closures, Up: Format and Handling of Formulas

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.

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

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.

— 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
     

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:

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


Next: , Previous: OFSF Operators, Up: Format and Handling of Formulas

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

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

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


Next: , Previous: DVFSF Operators, Up: Format and Handling of Formulas

3.5 ACFSF Operators

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

Note that the switch rlposden (see OFSF Operators) makes no sense for algebraically closed fields.


Next: , Previous: ACFSF Operators, Up: Format and Handling of Formulas

3.6 PASF Operators

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


Next: , Previous: PASF Operators, Up: Format and Handling of Formulas

3.7 IBALP Operators

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


Next: , Previous: IBALP Operators, Up: Format and Handling of Formulas

3.8 DCFSF Operators

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


Next: , Previous: DCFSF Operators, Up: Format and Handling of Formulas

3.9 Extended Built-in Commands

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

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

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.

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

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

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


Next: , 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.

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

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.

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


Previous: Global Switches, Up: Format and Handling of Formulas

3.11 Basic Functions on Formulas

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


Next: , Previous: Format and Handling of Formulas, Up: Top

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.


Next: , Up: Simplification

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

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


Next: , Up: Standard Simplifier 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.

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.

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

6.1.2 Cylindrical Algebraic Decomposition

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

6.1.3 Hermitian Quantifier Elimination

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


Next: , 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].

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

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.

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


Next: , 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].

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


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

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

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


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

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.


Next: , Previous: References, Up: Top

Functions


Next: , Up: Functions

Documentation of Functions


Previous: Documentation of Functions, Up: Functions

References to Functions


Next: , Previous: Functions, Up: Top

Switches and Variables


Next: , Up: Switches and Variables

Documentation of Switches and Variables

Short Contents

Table of Contents