xref: /dports/math/reduce/Reduce-svn5758-src/packages/redlog/texi/redlog.texi

\input texinfo
@c ----------------------------------------------------------------------
@c $Id: redlog.texi,v 1.25 2006/11/25 11:39:18 sturm Exp $
@c ----------------------------------------------------------------------
@c Copyright (c) 1995-2004 Andreas Dolzmann and Thomas Sturm
@c ----------------------------------------------------------------------
@c $Log: redlog.texi,v $
@c Revision 1.25  2006/11/25 11:39:18  sturm
@c makeinfo can produce html meanwhile. It produces better results than
@c texi2html. There are some odd constructions with @ifhtml/@ifnothtml at
@c the beginning of redlog.texi. For now this allows to automatically obtain
@c something nice for the Web page.
@c
@c Revision 1.24  2006/11/25 10:59:59  sturm
@c Bumped Edition 3.0->3.1, Version 3.0->3.6, Copyright 1995-2004->1995->2006.
@c Fixed a typo (g was missing in "Seidenberg").
@c
@c Revision 1.23  2004/11/20 16:00:09  seidl
@c Documented procedures rlcadporder, rlcadguessauto and switches
@c rlcadte, rlcadpbfvs.
@c
@c Revision 1.22  2004/08/30 10:39:33  lasaruk
@c Minor changes
@c
@c Revision 1.21  2004/08/29 22:36:44  lasaruk
@c Some switches documented
@c
@c Revision 1.20  2004/08/29 22:25:07  lasaruk
@c More PASF documentation done.
@c
@c Revision 1.19  2004/05/07 09:26:52  seidl
@c Added Quickstart. Added Bounded Quantifiers.  Corrected and added stuff
@c for PASF. TODO: look at examples in PASD-specific Simplification.
@c
@c Revision 1.18  2004/05/04 17:12:51  sturm
@c Quick switch to 3.0 as good as possible.
@c
@c Revision 1.17  2003/10/12 12:35:31  sturm
@c Some corrections in the doc of pasf.
@c Some doc on ibalp.
@c
@c Revision 1.16  2003/03/19 13:33:47  lasaruk
@c First version of PASF-documentation added.
@c
@c Revision 1.15  2003/03/10 18:50:27  seidl
@c Cared for PASF context and added TODO Lasaruk at several places.
@c Removed READ THIS FIRST hack. Now the following simple commands should
@c generate the desired info, dvi and html output:
@c   makeinfo redlog.texi
@c   tex redlog.texi
@c   texi2html -split_chapter -menu -expandinfo redlog.texi
@c For the online manual, index.html can link now to redlog.html instead
@c of redlog_toc.html. Other desired output forms have still to be looked
@c after.
@c
@c Revision 1.14  2002/08/29 08:12:04  dolzmann
@c Added description of local quantifier elimination.
@c
@c Revision 1.13  2002/01/18 12:39:26  sturm
@c Addded documentation for CAD.
@c
@c Revision 1.12  1999/04/13 22:17:30  sturm
@c Added remark on updates on the WWW page.
@c
@c Revision 1.11  1999/04/13 12:27:14  sturm
@c Removed a blank line within @itemize.
@c
@c Revision 1.10  1999/04/11 12:50:32  sturm
@c Removed reference to program documentation for now.
@c
@c Revision 1.9  1999/04/11 12:23:58  sturm
@c Overworked once more.
@c Better index.
@c Ispelled again.
@c
@c Revision 1.8  1999/04/07 17:05:39  sturm
@c Overworked chapter "Quantifier Elimination and Variants".
@c Ispelled.
@c
@c Revision 1.7  1999/04/05 12:49:12  sturm
@c Finished overworking chapter "Simplification".
@c Overworked chapter "Normal Forms".
@c Completely dropped chapter "Miscellaneous".
@c
@c Revision 1.6  1999/04/01 11:31:06  sturm
@c Overworked chapter "Simplification" and changed indeces.
@c
@c Revision 1.5  1999/03/22 16:48:07  sturm
@c Overworked chapter "Format and Handling of Formulas". There is only "Other
@c Stuff" left in chapter "Miscellaneous" now.
@c
@c Revision 1.4  1999/03/22 14:33:20  sturm
@c Updated references.
@c Overworked Introduction. New section "Loading and Context Selection".
@c
@c Revision 1.3  1998/04/09 11:14:38  sturm
@c Added documentation for switch rlqeqsc.
@c
@c Revision 1.2  1997/10/02 09:36:57  sturm
@c Updated reference to simplification paper.
@c
@c Revision 1.1  1997/08/18 17:22:50  sturm
@c Renamed "rl.texi" to this file "redlog.texi."
@c Changes due to renaming "rl.red" to "redlog.red."
@c
@c ----------------------------------------------------------------------
@c Revision 1.20  1997/08/14 10:10:54  sturm
@c Renamed rldecdeg to rldecdeg1.
@c Added service rldecdeg.
@c
@c Revision 1.19  1996/10/23 12:03:05  sturm
@c Added "exceptionlist" paramter to rlgqe and rlgqea. Several quantifier
@c blocks are treated correctly now.
@c
@c Revision 1.18  1996/10/22 11:17:05  dolzmann
@c Adapted the documentation of the procedures rlstruct, rlifstruct to
@c the new interface.
@c
@c Revision 1.17  1996/10/20 15:57:46  sturm
@c Added documentation for the switches rlnzden, rlposden, and rladdcond.
@c Added documentation for the functions rlvarl, rlfvarl, and rlbvarl.
@c
@c Revision 1.16  1996/10/09 14:46:29  sturm
@c Corrected @settitle.
@c
@c Revision 1.15  1996/10/09 11:41:04  sturm
@c Some more minor changes.
@c
@c Revision 1.14  1996/10/08 17:41:58  sturm
@c Overworked the whole thing more than once.
@c
@c Revision 1.13  1996/10/07 21:58:39  dolzmann
@c Added data structure substitution_list.
@c Added documentation for rlterml, rltermml, rlifacml, rltnf, rltnft,
@c rlstruct, and rlifstruct.
@c
@c Revision 1.12  1996/10/07 18:39:08  reiske
@c Revised and corrected documentation.
@c Added documentation for rlqeipo, rlqews, and rlgentheo.
@c Updated documentation for tableau and Groebner simplifier.
@c Added documentation for data structure "cdl" and "elimination_answer".
@c
@c Revision 1.11  1996/09/26 13:05:17  dolzmann
@c Minor changes in description of rltab.
@c
@c Revision 1.10  1996/09/26 12:14:27  sturm
@c Corrected wrong citation label.
@c
@c Revision 1.9  1996/08/01 12:05:18  reiske
@c Added documentation for rlifacl and rlapnf.
@c
@c Revision 1.8  1996/07/14 10:04:54  dolzmann
@c Updated documentation of the Groebner simplifier.
@c
@c Revision 1.7  1996/06/13 10:03:45  sturm
@c Added documentation for data structure "theory" and for procedures
@c "sub" and "rlgqe".
@c Moved "rlopt" into the Chapter on QE.
@c
@c Revision 1.6  1996/03/12 12:55:55  sturm
@c Changed title to "Redlog User Manual."
@c Many changes in introductory sections: Added functionality overview,
@c "Getting Started", modified the "Bug Report" section, introduced the
@c notion of a "context."
@c Corrected example in the description of rlpnf.
@c Many changes in QE documentation chapter.
@c Added documentation for data structure "multiplicity list", switch
@c rlqeheu, and functions rlmatrix, rlatl, and rlatml.
@c Added a "Data Structure Index."
@c Added new (bibliographic) reference.
@c
@c Revision 1.5  1996/03/04 14:50:26  dolzmann
@c Added description of switches rlgserf, rlbnfsac.
@c Removed description of switch rlbnfsb.
@c
@c Revision 1.4  1996/02/18 15:56:46  sturm
@c Adapted the documentation of rlsiexpla to new default setting T.
@c
@c Revision 1.3  1996/02/18 15:16:48  sturm
@c Added references.
@c Added introductions to chapters on QE and optimization.
@c Added concept index.
@c Added description of input facilities.
@c Modified description of switch rlqedfs.
@c Added description of switches rlbnfsb, rlbnfsm, rlsifac, rlsimpl,
@c rlsipw, rlsipo.
@c
@c Revision 1.2  1995/08/30  07:29:18  sturm
@c Many changes. Version passed to R.O.S.E. with the rl demo.
@c
@c Revision 1.1  1995/07/17  14:33:33  sturm
@c Initial check-in.
@c
@c ----------------------------------------------------------------------
@setfilename redlog.info

@ifnothtml
@settitle @sc{redlog} User Manual
@end ifnothtml
@c @setchapternewpage off
@smallbook
@defcodeindex rf
@defcodeindex rv
@defcodeindex rt

@ifnothtml
@ifinfo
This is the documentation of @sc{redlog}, a @sc{reduce} logic package.
Copyright @copyright{} 1995-2006 by A. Dolzmann, A. Seidl, and T. Sturm.
@end ifinfo
@end ifnothtml

@titlepage
@title{Redlog User Manual}
@subtitle A @sc{reduce} Logic Package
@subtitle Edition 3.1, for @sc{redlog} Version 3.06 (@sc{reduce} 3.8)
@subtitle 24 November 2006
@author by A. Dolzmann, A. Seidl, and T. Sturm
@page
@vskip 0pt plus 1filll
Copyright @copyright{} 1995-2006 by A. Dolzmann, A. Seidl, and
T. Sturm.
@end titlepage

@ifnothtml
@ifnottex
@node Top
@top REDLOG
@heading REDLOG
@sc{redlog} is a @sc{reduce} package containing algorithms on
first-order formulas. The current version is 3.06.
@end ifnottex
@end ifnothtml

@heading Quick Start
In case you hate long manuals and want to see something within a
minute type @t{reduce} in the command line. @sc{reduce} should start up.
Type the four commands @t{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 @t{a} and @t{b} such that the quadratic
polynomial @t{a*x^2+b*x+1} has a real root.

@ifnothtml

@heading Acknowledgments
We acknowledge with pleasure the superb support by Herbert Melenk and
Winfried Neun of the Konrad-Zuse-Zentrum fuer Informationstechnik
Berlin, Germany, during this project. Furthermore, we wish to mention
numerous valuable mathematical ideas contributed by Volker Weispfenning,
University of Passau, Germany.

@heading Redlog Home Page
@cindex @sc{www}
@cindex home page
There is a @sc{redlog} home page maintained at

@center @t{http://www.fmi.uni-passau.de/~redlog/}.

It contains information on @sc{redlog}, online versions of publications,
and a collection of examples that can be computed with @sc{redlog}. This
site will also be used for providing update
@cindex update
versions of @sc{redlog}.

@heading Support
@cindex support
For mathematical and technical support, contact

@center @t{redlog@@fmi.uni-passau.de}.

@heading Bug Reports and Comments
@cindex bug report
Send bug reports and comments to

@center @t{redlog@@fmi.uni-passau.de}.

Any hint or suggestion is welcome. In particular, we are interested in
practical problems to the solution of which @sc{redlog} has contributed.
@end ifnothtml

@ifhtml
@node Top
@top Contents
@end ifhtml
@menu
* Introduction::                         What is @sc{redlog}?
* Loading and Context Selection::
* Format and Handling of Formulas::      How to work with formulas.
* Simplification::                       Standard, tableau, and Groebner.
* Normal Forms::                         CNF, DNF, NNF, and PNF.
* Quantifier Elimination and Variants::  Elimination set methods.
* References::                           Further information on @sc{redlog}.
* Functions::
* Switches and Variables::
* Data Structures::
* Index::
@end menu

@node Introduction
@chapter Introduction
@sc{redlog} stands for @emph{@sc{reduce} logic system}. It provides an
extension of the computer algebra system @sc{reduce} to a @emph{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 @sc{redlog}
from the algebraic mode of @sc{reduce}. For a detailed
description of the system design see
@ifinfo
@ref{References,[DS97a]}.
@end ifinfo
@iftex
[DS97a].
@end iftex
@c There is an additional program documentation included in the @sc{reduce}
@c distribution.

An overview on some of the application areas of @sc{redlog} is given in
@ifinfo
@ref{References,[DSW98]}.
@end ifinfo
@iftex
[DSW98].
@end iftex
See also @ref{References} for articles on @sc{redlog}
applications.

@menu
* Contexts::
* Overview::
* Conventions::
@end menu

@node Contexts
@section Contexts
@cindex real numbers
@cindex complex numbers
@cindex p-adic number
@cindex real closed field
@cindex ordered field
@cindex real closed field
@cindex discretely valued field
@cindex algebraically closed field
@cindex contexts available
@cindex available contexts
@cindex @sc{ofsf}
@cindex @sc{acfsf}
@cindex @sc{dvfsf}
@sc{redlog} is designed for working with several @dfn{languages} and
@dfn{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:

@table @sc
@item ofsf
@sc{of} stands for @emph{ordered fields}, which is a little imprecise.
The quantifier elimination actually requires the more restricted class
of @emph{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 @sc{ofsf}.

@item dvfsf
@emph{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.

@item acfsf
@emph{Algebraically closed fields} such as the complex numbers.

@item pasf
@emph{Presburger Arithmetic}, i.e., the linear theory of integers
with congruences modulo
@tex
$m$
@end tex
@ifinfo
m
@end ifinfo
for
@tex
$m\geq1$
@end tex
@ifinfo
m>=2
@end ifinfo
.

@item ibalp
@emph{Initial Boolean algebras}, basically quantified propositional logic.

@item dcfsf
@emph{Differentially closed fields} according to Robinson. There is no
natural example. The quantifier elimination is an optimized version of
the procedure by Seidenberg (1956).
@end table

The trailing "@sc{-sf}" stands for @emph{standard form}, which is the
representation chosen for the terms within the implementation.
Accordingly, "@sc{-lp}" stands for @emph{Lisp prefix}.
@xref{Context Selection}, for details on selecting @sc{redlog}
contexts.

@node Overview
@section Overview
@sc{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:

@itemize @bullet
@item Numerous tools for comfortably inputing, decomposing, and
analyzing formulas. This includes, for instance, the construction of
systematic formulas via @code{for}-loops, and the extension of built-in
commands such as @code{sub}
@rfindex sub
or @code{part}.
@rfindex part
@xref{Format and Handling of Formulas}.

@item Several techniques for the @emph{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 @sc{ofsf}
@cindex @sc{ofsf}
and @sc{acfsf}
@cindex @sc{acfsf}
see
@ifinfo
@ref{References,[DS97]}.
@end ifinfo
@iftex
[DS97].
@end iftex
For the @sc{dvfsf}
@cindex @sc{dvfsf}
context see
@ifinfo
@ref{References,[DS99]}.
@end ifinfo
@iftex
[DS99].
@end iftex
@xref{Simplification}.

@item Various @emph{normal form computations}. The
@emph{@sc{cnf}/@sc{dnf}} computation includes both boolean and
algebraic simplification strategies
@ifinfo
@ref{References,[DS97]}.
@end ifinfo
@iftex
[DS97].
@end iftex
The @emph{prenex normal form} computation minimizes the number of
quantifier changes. @xref{Normal Forms}.

@item
@cindex comprehensive Groebner Basis
@cindex @sc{cgb}
@emph{Quantifier elimination} computes quantifier-free
equivalents for given first-order formulas.

For @sc{ofsf} and
@cindex @sc{ofsf}
@sc{dvfsf}
@cindex @sc{dvfsf}
we use a technique based on elimination set ideas
@ifinfo
@ref{References,[Wei88]}.
@end ifinfo
@iftex
[Wei88].
@end iftex
The @sc{ofsf}
@cindex @sc{ofsf}
implementation is restricted to at most quadratic occurrences of the
quantified variables, but includes numerous heuristic strategies for
coping with higher degrees. See
@ifinfo
@ref{References,[LW93]}, @ref{References,[Wei97]},
@end ifinfo
@iftex
[LW93], [Wei97]
@end iftex
for details on the method.
The @sc{dvfsf}
@cindex @sc{dvfsf}
implementation is restricted to formulas that are linear in the
quantified variables. The method is described in detail in
@ifinfo
@ref{References,[Stu00]}.
@end ifinfo
@iftex
[Stu00].
@end iftex

The @sc{acfsf}
@cindex @sc{acfsf}
quantifier elimination is based on @emph{comprehensive Groebner basis}
computation. There are no degree restrictions for this context
@ifinfo
@ref{References,[Wei92]}.
@end ifinfo
@iftex
[Wei92].
@end iftex
@xref{Quantifier Elimination}.

@item
@cindex geometric problem
@cindex network analysis
The contexts @sc{ofsf}
@cindex @sc{ofsf}
and @sc{acfsf}
@cindex @sc{acfsf}
allow a variant of quantifier
elimination called @dfn{generic quantifier elimination}
@ifinfo
@ref{References,[DSW98]}.
@end ifinfo
@iftex
[DSW98].
@end iftex
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
@ifinfo
@ref{References,[DSW98]}.
@end ifinfo
@iftex
[DSW98].
@end iftex
Generic quantifier elimination has turned out useful also for physical
applications such as network analysis
@ifinfo
@ref{References,[Stu97]}.
@end ifinfo
@iftex
[Stu97].
@end iftex
There is no generic quantifier elimination available for @sc{dvfsf}.
@cindex @sc{dvfsf}
@xref{Generic Quantifier Elimination}.

@item The contexts @sc{ofsf}
@cindex @sc{ofsf}
and @sc{dvfsf}
@cindex @sc{dvfsf}
provide variants of (generic) quantifier elimination that additionally
compute @dfn{answers}
@cindex answer
such as satisfying sample points for existentially
quantified formulas. This has been referred to as the "extended
quantifier elimination problem"
@ifinfo
@ref{References,[Wei97a]}.
@end ifinfo
@iftex
[Wei97a].
@end iftex
@xref{Quantifier Elimination}.

@item @sc{ofsf}
@cindex @sc{ofsf}
includes linear @emph{optimization} techniques based
on quantifier elimination
@ifinfo
@ref{References,[Wei94a]}.
@end ifinfo
@iftex
[Wei94a].
@end iftex
@xref{Linear Optimization}.
@end itemize

@node Conventions
@section Conventions
To avoid ambiguities with other packages, all @sc{redlog} functions and
switches are prefixed by "@code{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 @sc{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:

@table @dfn
@item Switch
@cindex 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.
@item Advanced Switch
@cindex advanced Switch
They are used like ordinary switches. You need, however, a good
knowledge about the underlying algorithms for making use of it.
@item Fix Switch
@cindex fix Switch
You do not want to change it.
@end table

@node Loading and Context Selection
@chapter Loading and Context Selection
@cindex starting @sc{redlog}

@menu
* Loading Redlog::
* Context Selection::
@end menu

@node Loading Redlog
@section Loading Redlog
@cindex loading @sc{redlog}
At the beginning of each session @sc{redlog} has to be loaded
explicitly. This is done by inputing the command @code{load_package
redlog;}
@rfindex load_package
from within a @sc{reduce} session.

@node Context Selection
@section Context Selection
@cindex theory
@cindex language
@cindex relations
@cindex predicates
@cindex functions
Fixing a context reflects the mathematical fact that first-order
formulas are defined over fixed @dfn{languages} specifying, e.g., valid
@dfn{function symbols} and @dfn{relation symbols} (@dfn{predicates}).
After selecting a language, fixing a @dfn{theory} such as "the theory of
ordered fields", allows to assign a semantics to the formulas. Both
language and theory make up a @sc{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 @sc{redlog} without specifying a context:

@smallexample
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
@end smallexample

@xref{Contexts}, for a summary of the available contexts @sc{ofsf},
@cindex @sc{ofsf}
@sc{dvfsf},
@cindex @sc{dvfsf}
@sc{acfsf},
@cindex @sc{acfsf}
@sc{pasf},
@cindex @sc{pasf}
@sc{ibalp}
@cindex @sc{ibalp}
and @sc{dcfsf}.
@cindex @sc{dcfsf}
A context can be selected by the @code{rlset} command:

@deffn {Function} rlset [@var{context} [@var{arguments}...]]
@deffnx {Function} rlset argument-list
@cindex language selection
@cindex context selection
@rtindex dvf_class_specification
Set current context. Valid choices for @var{context} are @sc{ofsf}
@cindex @sc{ofsf}
(ordered fields standard form), @sc{dvfsf}
@cindex @sc{dvfsf}
(discretely valued fields standard form), @sc{acfsf}
@cindex @sc{acfsf}
(algebraically closed fields standard form), @sc{pasf}
@cindex @sc{pasf}
(Presburger arithmetic standard form), @sc{ibalp}
@cindex @sc{ibalp}
(initial Boolean algebra Lisp prefix), and @sc{dcfsf}.
@cindex @sc{dcfsf}
With @sc{ofsf}, @sc{acfsf},
@sc{pasf}, @sc{ibalp}, and  @sc{dcfsf} there are no further arguments. With
@sc{dvfsf} an optional @var{dvf_class_specification} can be passed,
which defaults to @code{0}. @code{rlset} returns the old setting as a
list that can be saved to be passed to @code{rlset} later. When called
with no arguments (or the empty list), @code{rlset} returns the current
setting.
@end deffn

@deftp {Data Structure} {dvf_class_specification}
@cindex p-adic number
@cindex p-adic valuation
@cindex valuation (p-adic)
@cindex valued field
@cindex discretely valued field
Zero, or a possibly negative prime
@tex
$q$.
@end tex
@ifinfo
q.
@end ifinfo

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

For positive
@tex
$q$,
@end tex
@ifinfo
q,
@end ifinfo
all computations take place wrt.@: the corresponding
@tex
$q$-adic
@end tex
@ifinfo
q-adic
@end ifinfo
valuation.

For negative
@tex
$q$,
@end tex
@ifinfo
q,
@end ifinfo
the
@tex
"$-$"
@end tex
@ifinfo
"-"
@end ifinfo
can be read as ``up
to'', i.e., all computations are performed in such a way that they are
correct for all
@tex
$p$-adic
@end tex
@ifinfo
p-adic
@end ifinfo
valuations with
@tex
$p \leq |q|$.
@end tex
@ifinfo
p <= q.
@end ifinfo
In this case, the knowledge of an upper bound for
@tex
$p$
@end tex
@ifinfo
p
@end ifinfo
supports the
quantifier elimination @code{rlqe}/@code{rlqea}
@rfindex rlqe
@rfindex rlqea
@ifinfo
@ref{References,[Stu00]}.
@end ifinfo
@iftex
[Stu00].
@end iftex
@xref{Quantifier Elimination}.
@end deftp

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, @sc{redlog} provides a global variable
@code{rldeflang}, which contains a default context. This variable can be
set already @emph{before} loading @file{redlog}. This is typically done
within the @file{.reducerc} profile:
@cindex @file{.reducerc} profile

@example
lisp (rldeflang!* := '(ofsf));
@end example

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

@defvr Fluid rldeflang!*
@cindex language default
@cindex default language
@cindex context default
@cindex default context
Default language. This can be bound to a default context before loading
@file{redlog}. More precisely, @code{rldeflang!*} contains the arguments
of @code{rlset} as a Lisp list. If @code{rldeflang!*} is non-nil,
@code{rlset}
@rfindex rlset
is automatically executed on @code{rldeflang!*} when
loading @file{redlog}.
@end defvr

In addition, @sc{redlog} evaluates an environment variable
@code{RLDEFLANG}. This allows to fix a default context within the shell
already before starting @sc{reduce}. The syntax for setting environment
variables depends on the shell. For instance, in the @sc{gnu} Bash or in
the csh shell one would say @code{export RLDEFLANG=ofsf} or
@code{setenv RLDEFLANG ofsf}, respectively.

@defvr {Environment Variable} RLDEFLANG
@cindex language default
@cindex default language
@cindex context default
@cindex default context
Default language. This may be bound to a context in the sense of the
first argument of @code{rlset}.
@rfindex rlset
With @code{RLDEFLANG} set, any
@code{rldeflang!*}
@rvindex rldeflang!*
binding is overloaded.
@end defvr

@node Format and Handling of Formulas
@chapter Format and Handling of Formulas
After loading @sc{redlog} and selecting a context (@pxref{Loading and
Context Selection}), there are @emph{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.

@menu
* First-order Operators::
* Closures::
* OFSF Operators::
* DVFSF Operators::
* ACFSF Operators::
* PASF Operators::
* IBALP Operators::
* DCFSF Operators::
* Extended Built-in Commands::
* Global Switches::
* Basic Functions on Formulas::
@end menu

@node First-order Operators
@section First-order Operators

Though the operators @code{and}, @code{or}, and @code{not} are already
sufficient for representing boolean formulas, @sc{redlog} provides a
variety of other boolean operators for the convenient mnemonic input of
boolean formulas.

@deffn {Unary Operator} not
@deffnx {n-ary Infix Operator} and
@deffnx {n-ary Infix Operator} or
@deffnx {Binary Infix Operator} impl
@deffnx {Binary Infix Operator} repl
@deffnx {Binary Infix Operator} equiv
@cindex negation
@cindex conjunction
@cindex disjunction
@cindex implication
@cindex replication
@cindex equivalence
@cindex expression input
@cindex input facilities
@cindex boolean operator
The infix operator precedence is from
strongest to weakest: @code{and}, @code{or}, @code{impl}, @code{repl},
@code{equiv}.
@end deffn

@xref{Extended Built-in Commands}, for the description of extended
@code{for}-loop
@rfindex for
actions that allow to comfortably input large systematic
conjunctions and disjunctions.

@sc{reduce} expects the user to know about the precedence of @code{and}
over @code{or}. In analogy to @code{+} and @code{*}, there are thus no
parentheses output around conjunctions within disjunctions. The
following switch causes such subformulas to be bracketed anyway.
@xref{Conventions}, for the notion of a "fix switch".

@defvr {Fix Switch} rlbrop
@cindex bracket
@cindex expression output
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.
@end defvr

Besides the boolean operators introduced above, first-order logic
includes the well-known @dfn{existential quantifiers} and @dfn{universal
quantifiers}
@tex
"$\exists$" and "$\forall$".
@end tex
@ifinfo
"@emph{exists}" and "@emph{forall}".
@end ifinfo

@deffn {Binary Operator} ex
@deffnx {Binary Operator} all
@cindex quantifier
@cindex expression input
@cindex input facilities
These are the @dfn{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.
@end deffn

@xref{Closures}, for automatically quantifying all variables except for
an exclusion list.

@deffn {Binary Operator} bex
@deffnx {Binary Operator} ball
@cindex bounded quantifier
These are the @dfn{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 @sc{pasf}.
@end deffn

For convenience, we also have boolean constants
@cindex boolean constant
for the truth values.
@cindex truth value

@defvar true
@defvarx false
@cindex truth value
@cindex expression input
@cindex input facilities
These algebraic mode variables are reserved. They serve as @dfn{truth
values}.
@end defvar

@node Closures
@section Closures
@cindex closure

@defun rlall formula [@var{exceptionlist}]
@cindex universal closure
@cindex closure
@cindex quantifier
@cindex expression input
@cindex input facilities
Universal closure. @var{exceptionlist} is a list of variables empty by
default. Returns @var{formula} with all free variables universally
quantified, except for those in @var{exceptionlist}.
@end defun

@defun rlex formula [@var{exceptionlist}]
@cindex existential closure
@cindex closure
@cindex quantifier
@cindex expression input
@cindex input facilities
Existential closure. @var{exceptionlist} is a list of variables empty by
default. Returns @var{formula} with all free variables existentially
quantified, except for those in @var{exceptionlist}.
@end defun

@node OFSF Operators
@section OFSF Operators
@cindex ordered field
The @sc{ofsf}
@cindex @sc{ofsf}
context implements @emph{ordered fields} over the language of
@emph{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
@sc{ofsf} quantifier elimination procedures
@cindex quantifier elimination
(@pxref{Quantifier Elimination and Variants}) for non-linear formulas
actually operate over
@cindex real closed field
@emph{real closed fields}. See @ref{Contexts} and @ref{Context
Selection} for details on contexts.

@deffn {Binary Infix operator} equal
@deffnx {Binary Infix operator} neq
@deffnx {Binary Infix operator} leq
@deffnx {Binary Infix operator} geq
@deffnx {Binary Infix operator} lessp
@deffnx {Binary Infix operator} greaterp
@cindex equation
@cindex inequality
@cindex ordering
@cindex expression input
@cindex input facilities
The above operators may also be written as @code{=}, @code{<>},
@code{<=}, @code{>=}, @code{<}, and @code{>}, respectively. For @sc{ofsf}
@cindex @sc{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
@emph{chains}
@cindex chains of binary relations
of the above relations, which are also expanded immediately:

@smallexample
a<>b<c>d=f
     @result{} a-b <> 0 and b-c < 0 and c-d > 0 and d-f = 0
@end smallexample

Here, only adjacent terms are related to each other.
@end deffn

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.
@cindex 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 @emph{fix
switches}. @xref{Conventions}, for the classification of @sc{redlog}
switches.

@defvr Switch rlnzden
@defvrx Switch rlposden
@cindex inverse
@cindex reciprocal
@cindex division
@cindex denominator
@cindex parametric denominator
Non-zero/positive denominators. Both switches are off by default. If
both @code{rlnzden} and @code{rlposden} are on, the latter is active.
Activating one of them, allows the input of reciprocal terms. With
@code{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.

@smallexample
(a/b)+c=0 and (a/d)+c>0;
                                 2
     @result{} a + b*c = 0 and a*d + c*d  > 0
@end smallexample

Turning @code{rlposden} on, guarantees the reciprocals to be strictly
positive which allows simple, i.e.@: non-square, multiplication also
with ordering relations.

@smallexample
(a/b)+c=0 and (a/d)+c>0;
     @result{} a + b*c = 0 and a + c*d > 0
@end smallexample
@end defvr

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
@var{theory}
@rtindex theory
(@pxref{Standard Simplifier,theory}) to certain @sc{redlog} procedures.
Optionally, the system can be forced to add them to the formula at the
input stage:

@defvr Switch rladdcond
@cindex inverse
@cindex reciprocal
@cindex division
Add condition. This is off by default. With @code{rladdcond} on,
non-zeroness and positivity assumptions made due to the switches
@code{rlnzden} and @code{rlposden}
@rvindex rlnzden
@rvindex rlposden
are added to the formula at the input
stage. With @code{rladdcond} and @code{rlposden} on we get for instance:

@smallexample
(a/b)+c=0 and (a/d)+c>0;
     @result{} (b <> 0 and a + b*c = 0) and (d > 0 and a + c*d > 0)
@end smallexample
@end defvr

@node DVFSF Operators
@section DVFSF Operators
@cindex discretely valued field
Discretely valued fields are implemented as a one-sorted language using
the operators @code{|}, @code{||}, @code{~}, and @code{/~}, which encode
@tex
$\leq$, $<$, $=$, and $\neq$
@end tex
@ifinfo
@code{<=}, @code{<}, @code{=}, and @code{<>}
@end ifinfo
in the value group, respectively. For details see
@ifinfo
@ref{References,[Wei88]}, @ref{References,[Stu00]}, or @ref{References,[DS99]}.
@end ifinfo
@iftex
[Wei88], [Stu00], or [DS99].
@end iftex


@deffn {Binary Infix operator} equal
@deffnx {Binary Infix operator} neq
@deffnx {Binary Infix operator} div
@deffnx {Binary Infix operator} sdiv
@deffnx {Binary Infix operator} assoc
@deffnx {Binary Infix operator} nassoc
@cindex equation
@cindex inequality
@cindex divisibility
@cindex strict divisibility
@cindex weak divisibility
@cindex expression input
@cindex input facilities
The above operators may also be written as @code{=}, @code{<>},
@code{|}, @code{||}, @code{~}, and @code{/~}, respectively. Integer
reciprocals in the input are resolved correctly. @sc{dvfsf}
@cindex @sc{dvfsf}
allows the input of @emph{chains}
@cindex chains of binary relations
in analogy to @sc{ofsf}.
@cindex @sc{ofsf}
@xref{OFSF Operators}, for details.
@end deffn

With the @sc{dvfsf}
@cindex @sc{dvfsf}
operators there is no treatment of parametric denominators available.
@cindex denominator
@cindex parametric denominator

@node ACFSF Operators
@section ACFSF Operators
@deffn {Binary Infix operator} equal
@deffnx {Binary Infix operator} neq
@cindex equation
@cindex inequality
@cindex expression input
@cindex input facilities
@cindex @sc{acfsf}
The above operators may also be written as @code{=}, @code{<>}. As for
@sc{ofsf},
@cindex @sc{ofsf}
it is specified that all right hand sides must be zero. In
analogy to @sc{ofsf}, @sc{acfsf} allows also the input of @emph{chains}
@cindex chains of binary relations
and an appropriate treatment of parametric denominators
@cindex denominator
@cindex parametric denominator
in the input.
@xref{OFSF Operators}, for details.
@end deffn

Note that the switch @code{rlposden}
@rvindex rlposden
(@pxref{OFSF Operators}) makes no
sense for algebraically closed fields.

@node PASF Operators
@section PASF Operators

@deffn {Binary Infix operator} equal
@deffnx {Binary Infix operator} neq
@deffnx {Binary Infix operator} leq
@deffnx {Binary Infix operator} geq
@deffnx {Binary Infix operator} lessp
@deffnx {Binary Infix operator} greaterp
@cindex equation
@cindex inequality
@cindex ordering
@cindex congruence
@cindex expression input
@cindex input facilities
The above operators may also be written as @code{=}, @code{<>},
@code{<=}, @code{>=}, @code{<}, and @code{>}, respectively.
@end deffn

@deffn {Ternary Prefix operator} cong
@deffnx {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.
@smallexample
f := cong(x,0,2);
@group
  @result{} x ~2~ 0
@end group
@end smallexample
@end deffn

As for
@sc{ofsf},
@cindex @sc{ofsf}
it is specified that all right hand sides are transformed
to be zero. In analogy to @sc{ofsf}, @sc{pasf} allows
also the input of @emph{chains}
@cindex chains of binary relations in the input.
@xref{OFSF Operators}, for details.
@end deffn

@node IBALP Operators
@section IBALP Operators
@deffn {Unary operator} bnot
@deffnx {n-ary Infix operator} band
@deffnx {n-ary Infix operator} bor
@deffnx {Binary Infix operator} bimpl
@deffnx {Binary Infix operator} brepl
@deffnx {Binary Infix operator} bequiv
@cindex Boolean not
@cindex Boolean and
@cindex Boolean or
@cindex Boolean implication
@cindex Boolean replication
@cindex Boolean equivalence
The operator @code{bnot} may also be written as @code{~}. The operators
@code{band} and @code{bor} may also be written as @code{&} and @code{|},
resp. The operators @code{bimpl}, @code{brepl}, and @code{bequiv} may be
written as @code{->}, @code{<-}, and @code{<->}, resp.
@end deffn


@deffn {Binary Infix operator} equal
@cindex equation
The operator @code{equal} may also be written as @code{=}.
@end deffn

@node DCFSF Operators
@section DCFSF Operators
@deffn {Binary Infix operator} d
@cindex derivation
The operator @code{d} denotes (higher) derivatives in the sense of
differential algebra. For instance, the differential equation
@ifinfo

@example
x'^2 + x = 0
@end example

@end ifinfo
@tex
$$x'^2+x=0$$
@end tex
is input as @code{x d 1 ** 2 + x = 0}. @code{d} binds stronger than all
other operators.
@end deffn

@deffn {Binary Infix operator} equal
@deffnx {Binary Infix operator} neq
@cindex equation
@cindex inequality
The operator @code{equal} may also be written as @code{=}. The operator
@code{neq} may also be written as @code{<>}.
@end deffn

@node Extended Built-in Commands
@section Extended Built-in Commands

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

@deffn {for loop action} mkand
@deffnx {for loop action} mkor
@findex for
@cindex conjunction
@cindex disjunction
@cindex for loop action
@cindex expression input
@cindex input facilities
Make and/or. Actions for the construction of large systematic
conjunctions/disjunctions via for loops.

@smallexample
for i:=1:3 mkand
   for j:=1:3 mkor
      if j<>i then mkid(x,i)+mkid(x,j)=0;
           @result{} 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)
@end smallexample
@end deffn

Here the truth values
@cindex truth value
come into existence due to the internal
implementation of @code{for}-loops. They are always neutral in their
context, and can be easily removed via simplification (@pxref{Standard
Simplifier,function rlsimpl}, @pxref{Global Switches,switch rlsimpl}).

The @sc{reduce} substitution command @code{sub}
@rfindex sub
can be applied to formulas using the usual syntax.

@deftp {Data Structure} {substitution_list}
@var{substitution_list} is a list of equations each with a kernel left
hand side.
@end deftp

@defun sub substitution_list formula
@cindex substitution
@rtindex substitution_list
Substitute. Returns the formula obtained from @var{formula}
by applying the substitutions given by @var{substitution_list}.

@smallexample
sub(a=x,ex(x,x-a<0 and all(x,x-b>0 or ex(a,a-b<0))));
     @result{} ex x0 ( - x + x0 < 0 and all x0 (
             - b + x0 > 0 or ex a (a - b < 0)))
@end smallexample

@code{sub} works in such a way that equivalent formulas remain
equivalent after substitution. In particular, quantifiers are treated
correctly.
@end defun

@defun part formula n1 [n2 [n3...]]
Extract a part. The @code{part} of @var{formula} is implemented
analogously to that for built-in types: in particular the 0th part is
the operator.
@end defun

@iftex
Compare @code{rlmatrix} (@pxref{Basic Functions on Formulas})
@end iftex
@ifinfo
@xref{Basic Functions on Formulas,rlmatrix},
@end ifinfo
@rfindex rlmatrix
for extracting the @emph{matrix part} of a formula, i.e., removing
@emph{all} initial quantifiers.

@defun length formula
@cindex length
Length of @var{formula}. This is the number of arguments to the
top-level operator. The length is of particular interest with the n-ary
operators @code{and}
@rfindex and
and @code{or}.
@rfindex or
Notice that @code{part(@var{formula},length(@var{formula}))}
@rfindex part
is the part of largest index.
@end defun

@node Global Switches
@section Global Switches

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

@defvr Switch rlsimpl
@cindex automatic simplification
@cindex simplification
Simplify. By default this switch is off. With this switch on, the
function @code{rlsimpl}
@rfindex rlsimpl
is applied at the expression evaluation stage. @xref{Standard
Simplifier, rlsimpl}.
@end defvr

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.
@cindex normal form
For formulas, however, the
simplified equivalent is by no means canonical.

@defvr {Switch} rlrealtime
@cindex real time
@cindex time
@cindex wall clock time
Real time. By default this switch is off. If on it protocols the wall
clock time needed for @sc{redlog} commands in seconds. In contrast to
the built-in @code{time}
@rvindex time
switch, the time is printed @emph{above} the
result.
@end defvr

@defvr {Advanced Switch} rlverbose
@cindex verbosity output
@cindex protocol
Verbose. By default this switch is off. It toggles verbosity output with
some @sc{redlog} procedures. The verbosity output itself is not
documented.
@end defvr

@node Basic Functions on Formulas
@section Basic Functions on Formulas

@defun rlatnum formula
@cindex count atomic formulas
@cindex number of atomic formulas
@cindex atomic formulas
Number of atomic formulas. Returns the number of atomic formulas
contained in @var{formula}. Mind that truth values
@cindex truth value
are not considered
atomic formulas. In @sc{pasf} the amount of atomic
formulas in a bounded formula is computed
syntactically without expanding the bounds.
@end defun

@deftp {Data Structure} {multiplicity_list}
A list of 2-element-lists containing an object and the number of its
occurrences. Names of functions returning @var{multiplicity_lists}
typically end on "ml".
@end deftp

@defun rlatl formula
@cindex atomic formula list
@cindex list of atomic formulas
@cindex set of atomic formulas
@cindex atomic formulas
List of atomic formulas. Returns the set of atomic formulas contained in
@var{formula} as a list.
@end defun

@defun rlatml formula
@cindex atomic formula multiplicity list
@cindex multiplicity list of atomic formulas
@cindex atomic formulas
@rtindex multiplicity_list
Multiplicity list of atomic formulas. Returns the atomic formulas
contained in @var{formula} in a @var{multiplicity_list}.
@end defun

@defun rlifacl formula
@cindex factors (irreducible)
@cindex irreducible factors
@cindex irreducible factors list
@cindex list of irreducible factors
@cindex set of irreducible factors
@cindex factorization
List of irreducible factors. Returns the set of all irreducible factors
of the nonzero terms occurring in @var{formula}.

@smallexample
rlifacl(x**2-1=0);
    @result{} @{x + 1,x - 1@}
@end smallexample
@end defun

@defun rlifacml formula
@cindex factors (irreducible)
@cindex irreducible factors
@cindex irreducible factors multiplicity list
@cindex multiplicity list of irreducible factors
@cindex factorization
@rtindex multiplicity_list
Multiplicity list of irreducible factors. Returns the set of all
irreducible factors of the nonzero terms occurring in @var{formula} in a
@var{multiplicity_list}.
@end defun

@defun rlterml formula
@cindex term list
@cindex list of terms
List of terms. Returns the set of all nonzero terms occurring in
@var{formula}.
@end defun

@defun rltermml formula
@cindex term multiplicity list
@cindex multiplicity list of terms
@rtindex multiplicity_list
Multiplicity list of terms. Returns the set of all nonzero terms
occurring in @var{formula} in a @var{multiplicity_list}.
@end defun

@defun rlvarl formula
@cindex list(s) of variables
@cindex variable list(s)
@cindex set of variables
Variable lists. Returns both the list of variables occurring freely
@cindex free variables
and that of the variables occurring boundly
@cindex bound variables
in @var{formula} in a two-element list. Notice that the two member lists
are not necessarily disjoint.
@end defun

@defun rlfvarl formula
@cindex list(s) of variables
@cindex variable list(s)
@cindex free variables
Free variable list. Returns the variables occurring freely in
@var{formula} as a list.
@end defun

@defun rlbvarl formula
@cindex list(s) of variables
@cindex variable list(s)
@cindex bound variables
Bound variable list. Returns the variables occurring boundly in
@var{formula} as a list.
@end defun

@defun rlstruct formula [@var{kernel}]
@cindex formula structure
@cindex structure of formula
Structure of a formula. @var{kernel} is @code{v} by default. Returns a
list @code{@{f,sl@}}. @code{f} is constructed from @var{formula} by
replacing each occurrence of a term with a kernel constructed by
concatenating a number to @var{kernel}. The @var{substitution_list}
@rtindex substitution_list
@code{sl} contains all substitutions
@cindex substitution
to obtain @var{formula} from @code{f}.

@smallexample
rlstruct(x*y=0 and (x=0 or y>0),v);
     @result{} @{v1 = 0 and (v2 = 0 or v3 > 0),
        @{v1 = x*y,v2 = x,v3 = y@}@}
@end smallexample
@end defun

@defun rlifstruct formula [@var{kernel}]
@cindex factors (irreducible)
@cindex irreducible factors
@cindex formula structure
@cindex factorization
Irreducible factor structure of a formula. @var{kernel} is @code{v} by
default. Returns a list @code{@{f,sl@}}. @code{f} is constructed from
@var{formula} by replacing each occurrence of an irreducible factor with
a kernel constructed by adding a number to @var{kernel}. The returned
@var{substitution_list}
@rtindex substitution_list
@code{sl} contains all substitutions
@cindex substitution
to obtain @var{formula} from @code{f}.

@smallexample
rlstruct(x*y=0 and (x=0 or y>0),v);
     @result{} @{v1*v2 = 0 and (v1 = 0 or v2 > 0),
        @{v1 = x,v2 = y@}@}
@end smallexample
@end defun

@defun rlmatrix formula
@cindex matrix of a formula
@cindex remove quantifiers
Matrix computation. Drops all @emph{leading} quantifiers
@cindex quantifier
from @var{formula}.
@end defun

@node Simplification
@chapter Simplification
@cindex simplification
The goal of simplifying a first-order formula is to obtain an equivalent
formula over the same language that is somehow simpler. @sc{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 @sc{ofsf}
@cindex @sc{ofsf}
versions of these are described in
@iftex
[DS97].
@end iftex
@ifinfo
@ref{References,[DS97]}.
@end ifinfo

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

For @sc{dvfsf}
@cindex @sc{dvfsf}
there is no Groebner simplifier available. The parts of the standard
simplifier that are particular to valued fields are described in
@iftex
[DS99].
@end iftex
@ifinfo
@ref{References,[DS99]}.
@end ifinfo
The tableau simplification is straightforwardly derived from the
@emph{smart simplifications} described there.

@menu
* Standard Simplifier::  Fast and idempotent
* Tableau Simplifier::   Coping with often occurring terms
* Groebner Simplifier::  Detecting algebraic dependencies
@end menu

In @sc{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 @sc{ofsf}
@cindex @sc{ofsf}
in
@ifinfo
@ref{References,[DSW98]}.
@end ifinfo
@iftex
[DSW98].
@end iftex
A suitable variant is available also in @sc{acfsf}
@cindex @sc{acfsf}
but not in @sc{dvfsf}.
@cindex @sc{dvfsf}

@menu
* Degree Decreaser::
@end menu

@node Standard Simplifier
@section Standard Simplifier

The @dfn{Standard Simplifier} is a fast simplification algorithm that is
frequently called internally by other @sc{redlog} algorithms. It can be
applied automatically at the expression evaluation stage by turning on
the switch @code{rlsimpl}
@rvindex rlsimpl
(@pxref{Global Switches,switch rlsimpl}).

@deftp {Data Structure} theory
A list of atomic formulas assumed to hold.
@end deftp

@defun rlsimpl formula [@var{theory}]
@cindex simplification
@cindex standard simplifier
@rtindex theory
Simplify. @var{formula} is simplified recursively such that the result
is equivalent under the assumption that @var{theory} holds. Default for
@var{theory} is the empty theory @code{@{@}}. Theory inconsistency may
but need not be detected by @code{rlsimpl}. If @var{theory} is detected
to be inconsistent, a corresponding error is raised. Note that under an
inconsistent theory, @emph{any} formula is equivalent to the input,
i.e., the result is meaningless. @var{theory} should thus be chosen
carefully.
@end defun

@menu
* General Features of the Standard Simplifier::
* General Standard Simplifier Switches::
* OFSF-specific Simplifications::
* OFSF-specific Standard Simplifier Switches::
* ACFSF-specific Simplifications::
* ACFSF-specific Standard Simplifier Switches::
* DVFSF-specific Simplifications::
* DVFSF-specific Standard Simplifier Switches::
* PASF-specific Simplifications::
* PASF-specific Standard Simplifier Switches::
@end menu

@node General Features of the Standard Simplifier
@subsection General Features of the Standard Simplifier
The standard simplifier @code{rlsimpl} includes the following features
common to all contexts:

@itemize @bullet
@item
Replacement of atomic subformulas by simpler equivalents. These
equivalents are not necessarily atomic (switches @code{rlsiexpl},
@code{rlsiexpla},
@rvindex rlsiexpla
@rvindex rlsiexpl
@pxref{General Standard Simplifier Switches}). For
details on the simplification on the atomic formula level, see
@ref{OFSF-specific Simplifications}, @ref{ACFSF-specific
Simplifications}, and @ref{DVFSF-specific Simplifications}.
@item
Proper treatment of truth values.
@cindex truth value
@item
Flattening
@cindex flatten nested operators
@cindex involutive @code{not}
nested n-ary operator levels and resolving involutive
applications of @code{not}.
@rfindex not
@item
Dropping @code{not}
@rfindex not
operator with atomic formula arguments by changing
the relation of the atomic formula appropriately. The languages of all
contexts allow to do so.
@item
Changing @code{repl}
@rfindex repl
to @code{impl}.
@rfindex impl
@item
Producing a canonical ordering
@cindex canonical ordering
among the atomic formulas on a given
level (switch @code{rlsisort},
@rvindex rlsisort
@pxref{General Standard Simplifier
Switches}).
@item
Recognizing equal subformulas
@cindex equal subformulas
on a given level (switch @code{rlsichk},
@rvindex rlsichk
@pxref{General Standard Simplifier Switches}).
@item
Passing down information that is collected during recursion (switches
@code{rlsism},
@rvindex rlsism
@code{rlsiidem},
@rvindex rlsiidem
@pxref{General Standard Simplifier
Switches}). The technique of @dfn{implicit theories}
@cindex implicit theory
@cindex theory (implicit)
used for this is described in detail in
@iftex
[DS97]
@end iftex
@ifinfo
@ref{References,[DS97]},
@end ifinfo
for @sc{ofsf}/@sc{acfsf},
@cindex @sc{ofsf}
@cindex @sc{acfsf}
and in
@iftex
[DS99]
@end iftex
@ifinfo
@ref{References,[DS99]},
@end ifinfo
for @sc{dvfsf}.
@cindex @sc{dvfsf}
@item
Considering interaction of atomic formulas on the same level and
interaction with information inherited from higher levels (switch
@code{rlsism},
@rvindex rlsism
@pxref{General Standard Simplifier Switches}). The
@dfn{smart simplification}
@cindex smart simplification
techniques used for this are beyond the scope of this manual. They are
described in detail in
@iftex
[DS97]
@end iftex
@ifinfo
@ref{References,[DS97]},
@end ifinfo
for @sc{ofsf}/@sc{acfsf},
@cindex @sc{ofsf}
@cindex @sc{acfsf}
and in
@iftex
[DS99]
@end iftex
@ifinfo
@ref{References,[DS99]},
@end ifinfo
for @sc{dvfsf}.
@cindex @sc{dvfsf}
@end itemize

@node General Standard Simplifier Switches
@subsection General Standard Simplifier Switches

@defvr Switch rlsiexpla
@cindex explode terms
@cindex simplification
@cindex split atomic formula
@cindex additively split atomic formula
@cindex multiplicatively split atomic formula
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 @code{rlsipd}
@rvindex rlsipd
(@pxref{OFSF-specific Standard Simplifier Switches}). With
@code{rlsiexpla}
@rvindex rlsiexpla
on, we obtain:

@smallexample
f := (a - 1)**3 * (a + 1)**4 >=0;
         7    6      5      4      3      2
     @result{} a  + a  - 3*a  - 3*a  + 3*a  + 3*a  - a - 1 >= 0

rlsimpl f;
@rfindex rlsimpl
     @result{} a - 1 >= 0 or a + 1 = 0
@end smallexample

With @code{rlsiexpla} off, @code{f} will simplify as in the description
of the switch @code{rlsipd}. @code{rlsiexpla} is not used in the
@sc{dvfsf}
@cindex @sc{dvfsf}
context. The @sc{dvfsf} simplifier behaves like @code{rlsiexpla} on.
@end defvr

@defvr Switch rlsiexpl
@cindex simplification
@cindex explode terms
@cindex split atomic formula
@cindex additively split atomic formula
@cindex multiplicatively split atomic formula
Simplify explode. By default this switch is on. Its role is very similar
to that of @code{rlsiexpla},
@rvindex rlsiexpla
but it considers the operator the scope of
which the atomic formula occurs in: With @code{rlsiexpl} on

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

simplifies as in the description of the switch @code{rlsiexpla} whenever
it occurs in a disjunction, and it simplifies as in the description of
the switch @code{rlsipd}
@rvindex rlsipd
(@pxref{OFSF-specific Standard Simplifier Switches}) else.
@code{rlsiexpl} is not used in the @sc{dvfsf}
@cindex @sc{dvfsf}
context. The @sc{dvfsf} simplifier behaves like @code{rlsiexpla} on.
@end defvr

The user is not supposed to alter the settings of the following
@emph{fix switches} (@pxref{Conventions}):

@defvr {Fix Switch} rlsism
@cindex simplification
@cindex smart simplification
Simplify smart. By default this switch is on. See the description of the
function @code{rlsimpl}
@rfindex rlsimpl
(@pxref{Standard Simplifier}) for its effects.

@smallexample
rlsimpl(x>0 and x+1<0);
     @result{} false
@end smallexample
@end defvr

@defvr {Fix Switch} rlsichk
@cindex simplification
@cindex multiple occurrences
@cindex equal subformulas
Simplify check. By default this switch is on enabling checking for equal
sibling subformulas:

@smallexample
rlsimpl((x>0 and x-1<0) or (x>0 and x-1<0));
     @result{} (x>0 and x-1<0)
@rfindex rlsimpl
@end smallexample
@end defvr

@defvr {Fix Switch} rlsiidem
@cindex simplification
@cindex idempotent simplification
Simplify idempotent. By default this switch is on. It is relevant only
with switch @code{rlsism}
@rvindex rlsism
on. Its effect is that @code{rlsimpl}
@rfindex rlsimpl
(@pxref{Standard Simplifier}) is idempotent in the very most cases,
i.e., an application of @code{rlsimpl} to an already simplified formula
yields the formula itself.
@end defvr

@defvr {Fix Switch} rlsiso
@cindex simplification
@cindex sort atomic formulas
Simplify sort. By default this switch is on. It toggles the sorting of
the atomic formulas on the single levels.

@smallexample
rlsimpl((a=0 and b=0) or (b=0 and a=0));
@rfindex rlsimpl
     @result{} a = 0 and b = 0
@end smallexample
@end defvr

@node OFSF-specific Simplifications
@subsection OFSF-specific Simplifications
@cindex simplification of atomic formulas
@cindex atomic formula simplification
In the @sc{ofsf}
@cindex @sc{ofsf}
context, the atomic formula simplification includes the
following:

@itemize @bullet
@item
Evaluation of variable-free atomic formulas to truth values.
@cindex evaluate atomic formulas
@cindex variable-free atomic formula
@cindex truth value
@item
Make the left hand sides primitive over the integers
@cindex primitive over the integers
with positive head coefficient.
@cindex positive head coefficient
@item
Evaluation of trivial square sums
@cindex trivial square sum
to truth values (switch
@code{rlsisqf},
@rvindex rlsisqf
@pxref{OFSF-specific Standard Simplifier Switches}).
Additive splitting of trivial square sums (switch @code{rlsitsqspl},
@rvindex rlsitsqspl
@pxref{OFSF-specific Standard Simplifier Switches}).
@item
In ordering inequalities,
@cindex ordering inequality
@cindex ordering constraint
perform parity decomposition
@cindex parity decomposition
(similar to squarefree decomposition) of terms (switch @code{rlsipd},
@rvindex rlsipd
@pxref{OFSF-specific Standard Simplifier Switches}) with the option to
split an atomic formula
@cindex split atomic formula
@cindex multiplicatively split atomic formula
multiplicatively into two simpler ones (switches
@code{rlsiexpl} and @code{rlsiexpla},
@rvindex rlsiexpl
@rvindex rlsiexpla
@pxref{General Standard Simplifier Switches}).
@item
In equations and non-ordering inequalities,
@cindex non-ordering inequalities
replace left hand sides by their squarefree parts
@cindex squarefree part
(switch @code{rlsiatdv},
@rvindex rlsiatdv
@pxref{OFSF-specific
Standard Simplifier Switches}). Optionally, perform factorization
@cindex factorization
of equations and inequalities (switch @code{rlsifac},
@rvindex rlsifac
@pxref{OFSF-specific
Standard Simplifier Switches}, switches @code{rlsiexpl} and
@code{rlsiexpla}, @pxref{General Standard Simplifier Switches}).
@end itemize

For further details on the simplification in ordered fields see the
article
@iftex
[DS97].
@end iftex
@ifinfo
@ref{References,[DS97]}.
@end ifinfo

@node OFSF-specific Standard Simplifier Switches
@subsection OFSF-specific Standard Simplifier Switches

@defvr Switch rlsipw
@cindex simplification
@cindex prefer weak orderings
@cindex weak orderings
Simplification prefer weak orderings. Prefers weak orderings in contrast
to strict orderings
@cindex strict orderings
with implicit theory
@cindex implicit theory
simplification. @code{rlsipw} is off by default, which leads to the
following behavior:

@smallexample
rlsimpl(a<>0 and (a>=0 or b=0));
     @result{} a <> 0 and (a > 0 or b = 0)
@end smallexample

This meets the simplification goal of small satisfaction sets for the
atomic formulas. Turning on @code{rlsipw} will instead yield the
following:

@smallexample
rlsimpl(a<>0 and (a>0 or b=0));
     @result{} a <> 0 and (a >= 0 or b = 0)
@end smallexample
@end defvr

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

@defvr Switch rlsipo
@cindex simplification
@cindex prefer orderings
Simplification prefer orderings. Prefers orderings in contrast to
inequalities with implicit theory
@cindex implicit theory
simplification. @code{rlsipo} is on by default, which leads to the
following behavior:

@smallexample
rlsimpl(a>=0 and (a<>0 or b=0));
@rfindex rlsimpl
     @result{} a >= 0 and (a > 0 or b = 0)
@end smallexample

This meets the simplification goal of small satisfaction sets
@cindex small satisfaction sets
for the atomic formulas. Turning it on leads, e.g., to the following
behavior:

@smallexample
rlsimpl(a>=0 and (a>0 or b=0));
@rfindex rlsimpl
     @result{} a >= 0 and (a <> 0 or b = 0)
@end smallexample

Here, we meet the simplification goal of convenient relations
@cindex convenient relations
when orderings are considered inconvenient.
@end defvr

@defvr Switch rlsiatadv
@cindex simplification of atomic formulas
@cindex atomic formula simplification
@cindex advanced atomic formula simplification
Simplify atomic formulas advanced. By default this switch is on. Enables
sophisticated atomic formula simplifications based on squarefree part
@cindex squarefree part
computations and recognition of trivial square sums.
@cindex trivial square sum

@smallexample
rlsimpl(a**2 + 2*a*b + b**2 <> 0);
@rfindex rlsimpl
     @result{} a+b <> 0

rlsimpl(a**2 + b**2 + 1 > 0);
     @result{} true
@end smallexample

Furthermore, splitting of trivial square sums
@cindex split  trivial square sum
(switch @code{rlsitsqspl}),
@rvindex rlsitsqspl
parity decompositions
@cindex parity decomposition
(switch @code{rlsipd}),
@rvindex rlsipd
and factorization
@cindex factorization
of equations and inequalities (switch @code{rlsifac})
@rvindex rlsifac
are enabled.
@end defvr

@defvr Switch rlsitsqspl
@cindex trivial square sum
@cindex split trivial square sum
@cindex split atomic formula
@cindex additively split atomic formula
Simplify split trivial square sum. This is on by default. It is ignored
with @code{rlsiadv}
@rvindex rlsiadv
off. Trivial square sums are split additively
depending on @code{rlsiexpl} and @code{rlsiexpla}
@rvindex rlsiexpl
@rvindex rlsiexpla
(@pxref{General Standard Simplifier Switches}):

@smallexample
rlsimpl(a**2+b**2>0);
@rfindex rlsimpl
     @result{} a <> 0 or b <> 0
@end smallexample
@end defvr

@defvr Switch rlsipd
@cindex simplification
@cindex parity decomposition
Simplify parity decomposition. By default this switch is on. It is
ignored with @code{rlsiatadv}
@rvindex rlsiatadv
off. @code{rlsipd} toggles the parity decomposition of terms occurring
with ordering relations.
@cindex ordering relations

@smallexample
f := (a - 1)**3 * (a + 1)**4 >= 0;
         7    6      5      4      3      2
     @result{} a  + a  - 3*a  - 3*a  + 3*a  + 3*a  - a - 1 >= 0

rlsimpl f;
@rfindex rlsimpl
@group
         3    2
     @result{} a  + a  - a - 1 >= 0
@end group
@end smallexample

The atomic formula is possibly split into two parts according to the
setting of the switches @code{rlsiexpl} and @code{rlsiexpla}
@rvindex rlsiexpl
@rvindex rlsiexpla
(@pxref{General Standard Simplifier Switches}).
@end defvr

@defvr Switch rlsifac
@cindex simplification
@cindex factorization
Simplify factorization. By default this switch is on. It is ignored with
@code{rlsiatadv}
@rvindex rlsiatadv
off. Splits
@cindex split atomic formula
@cindex multiplicatively split atomic formula
equations and inequalities via factorization of their left hand side
terms into a disjunction or a conjunction, respectively. This is done in
dependence on @code{rlsiexpl} and @code{rlsiexpla}
@rvindex rlsiexpl
@rvindex rlsiexpla
(@pxref{General Standard Simplifier Switches}).
@end defvr

@node ACFSF-specific Simplifications
@subsection ACFSF-specific Simplifications
@cindex simplification of atomic formulas
@cindex atomic formula simplification
In the @sc{acfsf}
@cindex @sc{acfsf}
case the atomic formula simplification includes the following:

@itemize @bullet
@item
Evaluation of variable-free atomic formulas to truth values.
@cindex evaluate atomic formulas
@cindex variable-free atomic formula
@cindex truth value
@item
Make the left hand sides primitive over the integers
@cindex primitive over the integers
with positive head coefficient.
@cindex positive head coefficient
@item
Replace left hand sides of atomic formulas by their squarefree parts
@cindex squarefree part
(switch @code{rlsiatdv},
@rvindex rlsiatdv
@pxref{OFSF-specific Standard Simplifier Switches}). Optionally, perform
factorization
@cindex factorization
of equations and inequalities (switch @code{rlsifac},
@rvindex rlsifac
@pxref{OFSF-specific
Standard Simplifier Switches}, switches @code{rlsiexpl}
@rvindex rlsiexpl
and @code{rlsiexpla},
@rvindex rlsiexpla
@pxref{General Standard Simplifier Switches}).
@end itemize

For details see the description of the simplification for ordered fields
in
@iftex
[DS97].
@end iftex
@ifinfo
@ref{References,[DS97]}.
@end ifinfo
This can be easily adapted to algebraically closed fields.

@node ACFSF-specific Standard Simplifier Switches
@subsection ACFSF-specific Standard Simplifier Switches

The switches @code{rlsiatadv}
@rvindex rlsiatadv
and @code{rlsifac}
@rvindex rlsifac
have the same effects as in the @sc{ofsf}
@cindex @sc{ofsf}
context (@pxref{OFSF-specific
Standard Simplifier Switches}).

@node DVFSF-specific Simplifications
@subsection DVFSF-specific Simplifications
@cindex simplification of atomic formulas
@cindex atomic formula simplification
In the @sc{dvfsf}
@cindex @sc{dvfsf}
case the atomic formula simplification includes the following:

@itemize @bullet
@item
Evaluation of variable-free atomic formulas to truth values
provided that p is known.
@cindex evaluate atomic formulas
@cindex variable-free atomic formula
@cindex truth value
@item
Equations and inequalities can be treated as in @sc{acfsf}
@cindex @sc{acfsf}
(@pxref{ACFSF-specific Simplifications}). Moreover powers of p
@cindex power of p
@cindex cancel powers of p
can be cancelled.
@item
With valuation relations,
@cindex valuation relation
the @sc{gcd}
@cindex @sc{gcd}
@cindex greatest common divisor
@cindex cancel @sc{gcd}
of both sides is cancelled and
added appropriately as an equation or inequality.
@item
Valuation relations
@cindex valuation relation
involving zero sides can be evaluated or at least
turned into equations or inequalities.
@item
For concrete p, integer coefficients with valuation relations can be
replaced by a power of p
@cindex power of p
on one side of the relation.
@item
For unspecified p, polynomials in p can often be replaced by one
monomial.
@item
For unspecified p, valuation relations containing a monomial in p on one
side, and an integer on the other side can be transformed into @code{z ~
1} or @code{z /~ 1}, where @code{z} is an integer.
@end itemize

For details on simplification in p-adic fields see the article
@iftex
[DS99].
@end iftex
@ifinfo
@ref{References,[DS99]}.
@end ifinfo

Atomic formulas of the form @code{z ~ 1} or @code{z /~ 1}, where
@code{z} is an integer, can be split
@cindex split atomic formula
@cindex multiplicatively split atomic formula
into several ones via integer factorization.
@cindex integer factorization
@cindex 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:

@defun rlexplats formula
@cindex explode atomic formulas
@cindex split atomic formula
@cindex multiplicatively split atomic formula
Explode atomic formulas. Factorize
@cindex integer factorization
@cindex factorization
atomic formulas of the form @code{z ~ 1} or @code{z /~ 1}, where
@code{z} is an integer. @code{rlexplats} obeys the switches
@code{rlsiexpla}
@rvindex rlsiexpla
and @code{rlsiexpl}
@rvindex rlsiexpl
(@pxref{General Standard Simplifier Switches}), but not @code{rlsifac}
@rvindex rlsifac
(@pxref{DVFSF-specific Standard Simplifier Switches}).
@end defun

@node DVFSF-specific Standard Simplifier Switches
@subsection DVFSF-specific Standard Simplifier Switches

The context @sc{dvfsf}
@cindex @sc{dvfsf}
knows no special simplifier switches, and ignores the general switches
@code{rlsiexpla}
@rvindex rlsiexpla
and @code{rlsiexpl}
@rvindex rlsiexpl
(@pxref{General Standard Simplifier Switches}). It behaves like
@code{rlsiexpla} on. The simplifier contains numerous sophisticated
simplifications for atomic formulas in the style of @code{rlsiatadv}
@rvindex rlsiatadv
on (@pxref{OFSF-specific Standard Simplifier Switches}).

@defvr Switch rlsifac
@cindex simplification
@cindex factorization
@cindex integer factorization
Simplify factorization. By default this switch is on. Toggles certain
simplifications that require @emph{integer} factorization.
@xref{DVFSF-specific Simplifications}, for details.
@end defvr

@node PASF-specific Simplifications
@subsection PASF-specific Simplifications
@cindex simplification of atomic formulas
@cindex atomic formula simplification
Due to a simple term structure a lot simplification
can be performed on @sc{pasf} atomic formulas
with the total goal of reducing the absolute
summ of the coefficients.
In the @sc{pasf}
@cindex @sc{pasf}
context the atomic formula
simplification includes the following:

@itemize @bullet
@item
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.

@smallexample
f := cong(y+x+z,0,1);
rlsimpl f;
@rfindex rlsimpl
@group
     @result{} true
@end group
@end smallexample

@item
Modulo reduction. The coefficients of a @sc{pasf}
(in-)congurence modulo
@tex
$m$
@end tex
@ifinfo
m
@end ifinfo
can be reduced to be not greater than
@tex
$m-1$.
@end tex
@ifinfo
m-1
@end ifinfo
After the application of this simplification rule
all coefficients could vanish to zero.
@smallexample
f := cong(7*x+5*y,11,3);
rlsimpl f;
@rfindex rlsimpl
@group
     @result{} x + 2*y - 2 ~3~ 0
@end group
f := cong(8*x + 4*y, 16, 4);
rlsimpl f;
@rfindex rlsimpl
@group
     @result{} true
@end group
@end smallexample
@item
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.
@smallexample
f := 3 * x + 6 * y  - 9 = 0
rlsimpl f;
@rfindex rlsimpl
@group
     @result{} x + 2 * y - 3 = 0
@end group

f := 3 * x + 6 * y  - 7 < 0
rlsimpl f;
@rfindex rlsimpl
@group
     @result{} x + 2 * y - 2 <= 0
@end group

f := cong(3 * x + 6 * y - 3, 0, 9);
rlsimpl f;
@rfindex rlsimpl
@group
     @result{} x + 2 * y - 1 =~ 0 (3)
@end group
@end smallexample
@item
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.

@smallexample
f := 3*k-1 = 0;
rlsimpl f;
@rfindex rlsimpl
@group
     @result{} false
@end group
@end smallexample

@end itemize
Beyond atomic formulas simplification was extended to care for bounded
quantifiers.
@cindex bounded quantifers

@itemize @bullet

@item
@sc{pasf} provides a simplification procedure for bounds
using their special properties.

@item
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.

@item
Suitable atomic formulas in the matrix of a bounded
quantifier that contain the bounded variable
are moved inside the bound.

@item
Information from the bound is used to expand the implicit
theory for the matrix simplification.
@end itemize

@node PASF-specific Standard Simplifier Switches
@subsection PASF-specific Standard Simplifier Switches

@defvr Switch rlpasfsimplify
Simplifies the output formula after the elimination of each quantifier. By
default this switch is on.
@end defvr

@defvr 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.
@end defvr

@defvr Switch rlsiatadv
Turns the advanced PASF-speciefic simplification of atomic formulas
on. For details see @xref{PASF-specific Simplifications}.
@end defvr

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

@defvr Switch rlsusi
Turns the advanced @sc{susi} simplification on. Per default
this switch is on.
@end defvr

@node Tableau Simplifier
@section Tableau Simplifier

Although our standard simplifier (@pxref{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
@cindex change boolean structure
of a formula by constructing case distinctions.
@cindex case distinction
Compared to the standard simplifier they are much slower.
For details on tableau simplification see
@ifinfo
@ref{References,[DS97]}.
@end ifinfo
@iftex
[DS97].
@end iftex

@deftp {Data Structure} {cdl}
Case distinction list.
@cindex case distinction
This is a list of atomic formulas considered as a disjunction.
@end deftp

@defun rltab formula cdl
@cindex simplification
@cindex tableau
@rtindex cdl
Tableau method. The result is a tableau wrt.@: @var{cdl}, i.e., a
simplified equivalent of the disjunction over the specializations wrt.@:
all atomic formulas in @var{cdl}.

@smallexample
rltab((a = 0 and (b = 0 or (d = 0 and e = 0))) or
   (a = 0 and c = 0),@{a=0,a<>0@});
     @result{} (a = 0 and (b = 0 or c = 0 or (d = 0 and e = 0)))
@end smallexample
@end defun

@defun rlatab formula
@cindex simplification
@cindex tableau
@cindex automatic tableau
Automatic tableau method. Tableau steps wrt.@: a case distinction over
the signs of all terms occurring in @var{formula} are computed and the
best result, i.e., the result with the minimal number of atomic formulas
is returned.
@end defun

@defun rlitab formula
@cindex simplification
@cindex tableau
@cindex iterative tableau
Iterative automatic tableau method. @var{formula} is simplified by
iterative applications of @code{rlatab}.
@rfindex rlatab
The exact procedure depends on
the switch @code{rltabib}.
@rvindex rltabib
@end defun

@defvr Switch rltabib
@cindex simplification
@cindex tableau
@cindex branch-wise tableau iteration
Tableau iterate branch-wise. By default this switch is on. It controls
the procedure @code{rlitab}.
@rfindex rlitab
If @code{rltabib} is off, @code{rlatab}
@rfindex rlatab
is iteratively applied to the argument formula as long as shorter
results can be obtained. In case @code{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.
@end defvr

@node Groebner Simplifier
@section Groebner Simplifier
@cindex Groebner simplifier
The Groebner simplifier is not available in the @sc{dvfsf}
@cindex @sc{dvfsf}
context. It considers order theoretical and algebraic simplification
@cindex 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
@cindex Groebner basis
of certain subsets of terms occurring in the atomic formulas.

For calling the Groebner simplifier there are the following functions:

@defun rlgsc formula [@var{theory}]
@defunx rlgsd formula [@var{theory}]
@defunx rlgsn formula [@var{theory}]
@rtindex theory
@cindex normal form
@cindex boolean normal form
@cindex simplification
@cindex Groebner simplifier
@cindex polynomial reduction
@cindex reduce polynomials
Groebner simplifier. @var{formula} is a quantifier-free formula. Default
for @var{theory} is the empty theory @code{@{@}}. The functions differ
in the boolean normal form that is computed at the beginning.
@code{rlgsc} computes a conjunctive normal form,
@cindex conjunctive normal form
@cindex @sc{cnf}
@code{rlgsd} computes a disjunctive normal form,
@cindex disjunctive normal form
@cindex @sc{dnf}
and @code{rlgsn} heuristically decides for either a conjunctive or a
disjunctive normal form depending on the structure of @var{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.@: @var{theory}.

@smallexample
rlgsd(x=0 and ((y = 0 and x**2+2*y > 0) or
        (z=0 and x**3+z >= 0)));
    @result{} x = 0 and z = 0
@end smallexample

@smallexample
rlgsc(x neq 0 or ((y neq 0 or x**2+2*x*y <= 0) and
        (z neq 0 or x**3+z < 0)));
     @result{} x <> 0 or z <> 0
@end smallexample
@end defun

The heuristic used by @code{rlgsn}
@rfindex rlgsn
is intended to find the smaller boolean normal form
@cindex boolean normal form
among @sc{cnf} an @sc{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 @sc{reduce} to
compute the various Groebner bases. By default, the @code{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 @code{rlsimpl}
@rfindex rlsimpl
(@pxref{Standard Simplifier}), the Groebner simplifiers can in general
produce formulas containing more atomic formulas than the input. This
cannot happen if the switches @code{rlgsprod},
@rvindex rlgsprod
@code{rlgsred},
@rvindex rlgsred
and @code{rlgssub}
@rvindex rlgssub
are off and the input formula is a simplified boolean normal form.

The functionality of the Groebner simplifiers @code{rlgsc},
@rfindex rlgsc
@code{rlgsd},
@rfindex rlgsd
and @code{rlgsn}
@rfindex rlgsn
is controlled by numerous switches. In
most cases the default settings lead to a good simplification.

@defvr Switch rlgsrad
@cindex radical membership test
@cindex ideal membership test
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.
@end defvr

@defvr Switch rlgssub
@cindex substitution
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
@cindex complexity of terms
may increase or decrease independently.
@end defvr

@defvr Switch rlgsbnf
@cindex boolean normal form
@cindex normal form
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 @var{formula}.
@end defvr

@defvr Switch rlgsred
@cindex polynomial reduction
@cindex reduce polynomials
@cindex complexity of terms
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.
@end defvr

@defvr {Advanced Switch} rlgsvb
@cindex verbosity output
@cindex protocol
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 @code{rlverbose}
@rvindex rlverbose
(@pxref{Global Switches}) and @code{rlgsvb} are on.
@end defvr

@defvr {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
@cindex unsplit atomic formulas
@cindex contract atomic formulas
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 @code{rlgsprod} off.
@end defvr

@defvr {Advanced Switch} rlgserf
Groebner simplifier evaluate reduced form.
@cindex evaluate reduced form
By default this switch is on. It controls the evaluation of the atomic
formulas
@cindex evaluate atomic formulas
to truth values.
@cindex truth value
If this switch is on, the standard simplifier (@pxref{Standard
Simplifier})
@cindex standard simplifier
is used to evaluate atomic formulas. Otherwise atomic formulas are
evaluated only if their left hand side is a domain element.
@end defvr

@defvr {Advanced Switch} rlgsutord
@cindex term order
Groebner simplifier user defined term order. By default this switch is
off. Then all Groebner basis computations and reductions
@cindex polynomial reduction
@cindex reduce polynomials
are performed with respect to the @code{revgradlex}
@cindex @code{revgradlex}
term order. If this switch is on, the Groebner simplifier minds the term
order selected with the @code{torder}
@rfindex torder
statement. For passing a variable list to @code{torder}, note that
@code{rlgsradmemv!*}
@vrindex rlgsradmemv!*
is used as the tag variable for radical membership tests.
@cindex radical membership test
@end defvr

@defvr {Fluid} rlgsradmemv!*
@cindex radical membership test
Radical membership test variable. This fluid contains the tag variable
@cindex tag variable
used for the radical membership test with switch @code{rlgsrad}
@rvindex rlgsrad
on. It can be used to pass the variable explicitly to @code{torder}
@rfindex torder
with switch @code{rlgsutord}
@rvindex rlgsutord
on.
@end defvr

@node Degree Decreaser
@section Degree Decreaser
@cindex degree
@cindex degree restriction
The quantifier elimination procedures of @sc{redlog} (@pxref{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 @sc{dvfsf}
@cindex @sc{dvfsf}
context available.

@defun rldecdeg formula
Decrease degrees.
@cindex decrease degree
Returns a formula equivalent to @var{formula},
hopefully decreasing the degrees of the bound variables. In the
@sc{ofsf}
@cindex @sc{ofsf}
context there are in general some sign conditions
@cindex sign conditions
on the variables added, which slightly increases the number of contained
atomic formulas.

@smallexample
rldecdeg ex(@{b,x@},m*x**4711+b**8>0);
    @result{} ex b (b >= 0 and ex x (b + m*x > 0))
@end smallexample
@end defun

@defun rldecdeg1 formula [@var{varlist}]
@cindex decrease degree
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 @var{varlist},
where the empty @var{varlist} selects @emph{all} free variables of
@code{f}. The return value is a list @code{@{f,l@}}. @code{f} is a
formula, and @code{l} is a list @code{@{...,@{v,d@},...@}}, where
@code{v} is from @var{varlist} and @code{d} is an integer. @code{f} has
been obtained from @var{formula} by substituting
@cindex substitution
@code{v} for @code{v**d}. The sign conditions necessary with the
@sc{ofsf}
@cindex @sc{ofsf}
context are not generated automatically, but have to be
constructed by hand for the variables @code{v} with even degree @code{d}
in @code{l}.

@smallexample
rldecdeg1(m*x**4711+b**8>0,@{b,x@});
    @result{} @{b + m*x > 0,@{@{x,4711@},@{b,8@}@}@}
@end smallexample
@end defun

@node Normal Forms
@chapter Normal Forms

@menu
* Boolean Normal Forms::  CNF and DNF
* Miscellaneous Normal Forms::    Negation, prenex, anti-prenex
@end menu

@node Boolean Normal Forms
@section Boolean Normal Forms

For computing small boolean normal forms,
@cindex boolean normal form
see also the documentation of
the procedures @code{rlgsc}
@rfindex rlgsc
and @code{rlgsd}
@rfindex rlgsd
(@ref{Groebner Simplifier}).

@defun rlcnf formula
@cindex normal form
@cindex conjunctive normal form
@cindex @sc{cnf}
Conjunctive normal form. @var{formula} is a quantifier-free formula.
Returns a conjunctive normal form of @var{formula}.

@smallexample
rlcnf(a = 0 and b = 0 or b = 0 and c = 0);
    @result{} (a = 0 or c = 0) and b = 0
@end smallexample
@end defun

@defun rldnf formula
@cindex normal form
@cindex disjunctive normal form
@cindex @sc{dnf}
Disjunctive normal form. @var{formula} is a quantifier-free formula.
Returns a disjunctive normal form of @var{formula}.

@smallexample
rldnf((a = 0 or b = 0) and (b = 0 or c = 0));
    @result{} (a = 0 and c = 0) or b = 0
@end smallexample
@end defun

@defvr Switch rlbnfsm
@cindex boolean normal form
@cindex smart @sc{bnf} computation
@cindex simplifier recognized implication
Boolean normal form smart. By default this switch is off. If on,
@emph{simplifier recognized implication}
@cindex simplifier recognized implication
@ifinfo
(@pxref{References,[DS97]})
@end ifinfo
@iftex
[DS97]
@end iftex
is applied by @code{rlcnf}
@rfindex rlcnf
and @code{rldnf}.
@rfindex rldnf
This leads to smaller normal forms but is considerably time consuming.
@end defvr

@defvr {Fix Switch} rlbnfsac
@cindex boolean normal form
@cindex subsumption
@cindex cut
Boolean normal forms subsumption and cut. By default this switch is on.
With boolean normal form computation, subsumption and cut strategies are
applied by @code{rlcnf}
@rfindex rlcnf
and @code{rldnf}
@rfindex rldnf
to decrease the number of clauses.
@cindex decrease number of clauses
We give an example:

@smallexample
rldnf(x=0 and y<0 or x=0 and y>0 or x=0 and y<>0 and z=0);
    @result{} (x = 0 and y <> 0)
@end smallexample
@end defvr

@node Miscellaneous Normal Forms
@section Miscellaneous Normal Forms

@defun rlnnf formula
@cindex normal form
@cindex negation normal form
@cindex @sc{nnf}
Negation normal form. Returns a @dfn{negation normal form} of
@var{formula}. This is an @code{and}-@code{or}-combination of atomic
formulas. Note that in all contexts, we use languages
@cindex language
such that all
negations can be encoded by relations (@pxref{Format and Handling of
Formulas}). We give an example:

@smallexample
rlnnf(a = 0 equiv b > 0);
    @result{} (a = 0 and b > 0) or (a <> 0 and b <= 0)
@end smallexample

@code{rlnnf} accepts formulas containing quantifiers, but it does not
eliminate quantifiers.
@cindex quantifier
@end defun

@defun rlpnf formula
@cindex normal form
@cindex prenex normal form
@cindex @sc{pnf}
Prenex normal form. Returns a prenex normal form of @var{formula}. The
number of quantifier changes
@cindex quantifier changes
in the result is minimal among all prenex
normal forms that can be obtained from @var{formula} by only moving
quantifiers to the outside.

When @var{formula} contains two quantifiers with the same variable such
as in
@ifinfo

@example
ex x (x = 0) and ex x (x <> 0)
@end example

@end ifinfo
@tex
$$\exists x(x = 0) \land \exists x (x \neq 0)$$
@end tex
there occurs a name conflict. It is resolved according to the following
rules:
@cindex rename variables
@cindex variable renaming

@itemize @bullet
@item Every bound variable that stands in conflict with any other
variable is renamed.
@item Free variables are never renamed.
@end itemize

Hence @code{rlpnf} applied to the above example formula yields

@smallexample
rlpnf(ex(x,x=0) and ex(x,x<>0));
    @result{} ex x0 ex x1 (x0 = 0 and x1 <> 0)
@end smallexample
@end defun

@defun rlapnf formula
@cindex anti-prenex normal form
@cindex move quantifiers inside
@cindex prenex normal form
Anti-prenex normal form. Returns a formula equivalent to @var{formula}
where all quantifiers are moved to the inside as far as possible.
@cindex quantifier
@cindex move quantifiers inside

@smallexample
rlapnf ex(x,all(y,x=0 or (y=0 and x=z)));
    @result{} ex x (x = 0) or (all y (y = 0) and ex x (x - z = 0))
@end smallexample
@end defun

@defun rltnf formula terml
@cindex normal form
@cindex term normal form
Term normal form. @var{terml} is a list of terms. This combines @sc{dnf}
@cindex @sc{dnf}
@cindex disjunctive normal form
computation with tableau
@cindex tableau
ideas (@pxref{Tableau Simplifier}). A typical
choice for @var{terml} is @code{rlterml} @var{formula}.
@rfindex rlterml
If the switch @code{rltnft}
@rvindex rltnft
is off, then @code{rltnf(@var{formula},rlterml @var{formula})} returns a
@sc{dnf}.
@end defun

@defvr Switch rltnft
@cindex term normal form
Term normal form tree variant. By default this switch is on causing
@code{rltnf} to return a deeply nested formula.
@cindex deeply nested formula
@end defvr

@node Quantifier Elimination and Variants
@chapter Quantifier Elimination and Variants
@cindex comprehensive Groebner Basis
@cindex @sc{cgb}
@emph{Quantifier elimination} computes quantifier-free equivalents
@cindex quantifier-free equivalent
for given first-order formulas.

For @sc{ofsf}
@cindex @sc{ofsf}
there are two methods available:
@enumerate
@item
Virtual substitution
@cindex virtual substitution
based on elimination set
@cindex elimination set
ideas
@ifinfo
@ref{References,[Wei88]}.
@end ifinfo
@iftex
[Wei88].
@end iftex
This implementation is restricted to at most quadratic occurrences of the
quantified variables, but includes numerous heuristic strategies for
coping with higher degrees. See
@ifinfo
@ref{References,[LW93]}, @ref{References,[Wei97]},
@end ifinfo
@iftex
[LW93], [Wei97]
@end iftex
for details of the method.
@item
Partial cylindrical algebraic decomposition
@cindex cylindrical algebraic decomposition
@cindex partial cylindrical algebraic decomposition
(CAD)
@cindex CAD
introduced by Collins and Hong
@ifinfo
@ref{References,[CH91]}.
@end ifinfo
@iftex
[CH91].
@end iftex
There are no degree restrictions with CAD.
@end enumerate

For @sc{dvfsf}
@cindex @sc{dvfsf}
we use the virtual substitution method
@cindex virtual substitution
that is also available for
@sc{ofsf}.
@cindex @sc{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
@ifinfo
@ref{References,[Stu00]}.
@end ifinfo
@iftex
[Stu00].
@end iftex

The @sc{acfsf}
@cindex @sc{acfsf}
quantifier elimination is based on @emph{comprehensive
Groebner basis}
@cindex comprehensive Groebner basis
computation; there are no degree restrictions
@cindex degree restriction
for this context
@ifinfo
@ref{References,[Wei92]}.
@end ifinfo
@iftex
[Wei92].
@end iftex

In @sc{pasf} context the quantifier elimination is based
on the fast method similar to elimination by
virtual substitution introduced by Weispfenning. For
more details see
@ifinfo
@ref{References,[Wei90]}
@end ifinfo
@iftex
[Wei90].
@end iftex

@menu
* Quantifier Elimination::
* Generic Quantifier Elimination::
* Local Quantifier Elimination::
* Linear Optimization::
@end menu

@node Quantifier Elimination
@section Quantifier Elimination

@subsection Virtual Substitution

@defun rlqe formula [@var{theory}]
@rtindex theory
@cindex quantifier elimination
Quantifier elimination by virtual substitution. Returns a
quantifier-free equivalent
@cindex quantifier-free equivalent
of @var{formula} (wrt.@: @var{theory}). In the contexts @sc{ofsf}
@cindex @sc{ofsf}
and @sc{dvfsf},
@cindex @sc{dvfsf}
@var{formula} has to obey certain degree restrictions.
@cindex degree restriction
There are various techniques for decreasing the degree
@cindex decrease 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.
@end defun

For degree decreasing
@cindex decrease degree
heuristics see, e.g., @ref{Degree Decreaser}, or the switches
@code{rlqeqsc}/@code{rlqesqsc}.
@rvindex rlqeqsc
@rvindex rlqesqsc

@deftp {Data Structure} {elimination_answer}
A list of @dfn{condition--solution pairs},
@cindex condition--solution pairs
i.e., a list of pairs consisting of a quantifier-free formula and a set
of equations.
@end deftp

@defun rlqea formula [@var{theory}]
@rtindex theory
@cindex quantifier elimination
@cindex solution points
@cindex extended quantifier elimination
@cindex answer
@cindex sample solution
@rtindex elimination_answer
Quantifier elimination with answer. Returns an
@ifinfo
@var{elimination_answer}
@end ifinfo
@iftex
@var{elim@-i@-na@-tion_an@-swer}
@end iftex
obtained the following way: @var{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:

@itemize @bullet
@item In case the considered block is existential, for each evaluation
of the free variables we know the following: Whenever a @dfn{condition}
holds, then @var{formula} is @code{true}
@rvindex true
under the given evaluation, and the
@dfn{solution}
@cindex solution
is @emph{one} possible evaluation for the outer block variables
satisfying the matrix.
@item The universally quantified case is dual: Whenever a @dfn{condition}
is false, then @var{formula} is @code{false},
@rvindex false
and the @dfn{solution} is @emph{one} possible counterexample.
@cindex counterexample
@end itemize

As an example we show how to find conditions and solutions for a system
of two linear constraints:

@smallexample
rlqea ex(x,x+b1>=0 and a2*x+b2<=0);
           2                                    - b2
    @result{} @{@{a2 *b1 - a2*b2 >= 0 and a2 <> 0,@{x = -------@}@},
                                                a2
        @{a2 < 0 or (a2 = 0 and b2 <= 0),@{x = infinity1@}@}@}
@end smallexample

The answer can contain constants named @code{infinity}
@cindex @code{infinity}
or @code{epsilon},
@cindex @code{epsilon}
both indexed by a number: All @code{infinity}'s are positive and
infinite, and all @code{epsilon}'s are positive and infinitesimal wrt.@:
the considered field. Nothing is known about the ordering among the
@code{infinity}'s and @code{epsilon}'s though this can be relevant for
the points to be solutions. With the switch @code{rounded}
@rvindex rounded
on, the @code{epsilon}'s are evaluated to zero. @code{rlqea} is not
available in the context @sc{acfsf}.
@cindex @sc{acfsf}
@end defun

@defvr {Switch} rlqeqsc
@defvrx Switch rlqesqsc
@cindex quantifier elimination
@cindex quadratic special case
@cindex super quadratic special case
Quantifier elimination (super) quadratic special case. By default these
switches are off. They are relevant only in @sc{ofsf}.
@cindex @sc{ofsf}
If turned on, alternative elimination sets are used for certain special
cases by @code{rlqe}/@code{rlqea}
@rfindex rlqe
@rfindex rlqea
and @code{rlgqe}/@code{rlgqea}.
@rfindex rlgqe
@rfindex rlgqea
(@pxref{Generic Quantifier Elimination}). They will possibly avoid
violations of the degree restrictions,
@cindex degree restriction
but lead to larger results in general. Former versions of @sc{redlog}
without these switches behaved as if @code{rlqeqsc} was on and
@code{rlqesqsc} was off.
@end defvr

@defvr {Advanced Switch} rlqedfs
@cindex quantifier elimination
@cindex depth first search
@cindex breadth first search
Quantifier elimination depth first search. By default this switch is
off. It is also ignored in the @sc{acfsf}
@cindex @sc{acfsf}
context. It is ignored with the switch @code{rlqeheu}
@rvindex rlqeheu
on, which is the default for @sc{ofsf}.
@cindex @sc{ofsf}
Turning @code{rlqedfs} on makes @code{rlqe}/@code{rlqea}
@rfindex rlqe
@rfindex rlqea
and
@code{rlgqe}/@code{rlgqea}
@rfindex rlgqe
@rfindex rlgqea
(@pxref{Generic Quantifier Elimination}) work in a depth first search
manner instead of breadth first search. This saves space,
@cindex save space
and with decision problems,
@cindex decision problem
where variable-free atomic formulas can be evaluated
@cindex evaluate atomic formulas
to truth values,
@cindex truth value
it might save time.
@cindex save time
In general, it leads to larger results.
@end defvr

@defvr {Advanced Switch} rlqeheu
@cindex heuristic
@cindex search heuristic
@cindex quantifier elimination
@cindex depth first search
@cindex breadth first search
Quantifier elimination search heuristic. By default this switch is on in
@sc{ofsf}
@cindex @sc{ofsf}
and off in @sc{dvfsf}.
@cindex @sc{dvfsf}
It is ignored in @sc{acfsf}.
@cindex @sc{acfsf}
Turning @code{rlqeheu} on causes the switch @code{rlqedfs}
@rvindex rlqedfs
to be ignored. @code{rlqe}/@code{rlqea}
@rfindex rlqe
@rfindex rlqea
and @code{rlgqe}/@code{rlgqea}
@rfindex rlgqe
@rfindex rlgqea
(@pxref{Generic Quantifier Elimination}) will then decide between
breadth first search and depth first search for each quantifier block,
@cindex quantifier block
where @sc{dfs} is chosen when the problem is a decision problem.
@cindex decision problem
@end defvr

@defvr {Advanced Switch} rlqepnf
@cindex quantifier elimination
@cindex prenex normal form
Quantifier elimination compute prenex normal form. By default this
switch is on, which causes that @code{rlpnf}
@rfindex rlpnf
(@pxref{Miscellaneous Normal Forms}) is applied to @var{formula} before
starting the elimination process. If the argument formula to
@code{rlqe}/@code{rlqea}
@rfindex rlqe
@rfindex rlqea
or @code{rlgqe}/@code{rlgqea}
@rfindex rlgqe
@rfindex rlgqea
(@pxref{Generic Quantifier Elimination}) is already prenex, this switch
can be turned off. This may be useful with formulas containing
@code{equiv}
@rfindex equiv
since @code{rlpnf} applies @code{rlnnf},
@rfindex rlnnf
(@pxref{Miscellaneous Normal Forms}), and resolving equivalences can
double the size of a formula. @code{rlqepnf} is ignored in @sc{acfsf},
@cindex @sc{acfsf}
since @sc{nnf} is necessary for elimination there.
@end defvr

@defvr {Fix Switch} rlqesr
@cindex separate roots
Quantifier elimination separate roots. This is off by default. It is
relevant only in @sc{ofsf}
@cindex @sc{ofsf}
for @code{rlqe}/@code{rlgqe}
@rfindex rlqe
@rfindex rlqea
and for all but
the outermost quantifier block in @code{rlqea}/@code{rlgqea}.
@rfindex rlgqe
@rfindex rlgqea
For @code{rlqea} and @code{rlgqea} see @ref{Generic Quantifier
Elimination}. It affects the technique for substituting
@cindex substitution
the two solutions of a quadratic constraint
@cindex quadratic constraint
during elimination.
@end defvr

The following two functions @code{rlqeipo}
@rfindex rlqeipo
and @code{rlqews}
@rfindex 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 @code{rlqe}
@rfindex rlqe
has turned out superior.

@defun rlqeipo formula [@var{theory}]
@rtindex theory
@cindex quantifier elimination
@cindex prenex normal form
@cindex anti-prenex normal form
Quantifier elimination by virtual substitution in position. Returns a
quantifier-free equivalent
@cindex quantifier-free equivalent
to @var{formula} by iteratively making @var{formula} anti-prenex
(@pxref{Miscellaneous Normal Forms}) and eliminating one quantifier.
@end defun

@defun rlqews formula [@var{theory}]
@rtindex theory
@cindex quantifier elimination
@cindex prenex normal form
@cindex anti-prenex normal form
Quantifier elimination by virtual substitution with selection.
@var{formula} has to be prenex, if the switch @code{rlqepnf}
@rvindex rlqepnf
is off. Returns a quantifier-free
equivalent
@cindex quantifier-free equivalent
to @var{formula} by iteratively selecting a quantifier from the
innermost block, moving it inside as far as possible, and then
eliminating it. @code{rlqews} is not available in @sc{acfsf}.
@cindex @sc{acfsf}
@end defun

@subsection Cylindrical Algebraic Decomposition
@cindex cylindrical algebraic decomposition

@defun rlcad formula
@cindex quantifier elimination
@cindex cylindrical algebraic decomposition
Cylindrical algebraic decomposition. Returns a quantifier-free
equivalent of @var{formula}. Works only in context OFSF. There are no
degree restrictions on @var{formula}.
@rvindex rlcad
@end defun

@defun rlcadporder formula
@cindex projection order
Efficient projection order. Returns a list of variables. The first
variable is eliminated first.
@rvindex rlcadporder
@end defun

@defun rlcadguessauto formula
@cindex guess full CAD size
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.
@rvindex rlcadguessauto
@end defun

@defvr {Advanced Switch} rlcadfac
Factorisation.
This is on by default.
@rvindex rlcadfac
@end defvr

@defvr Switch rlcadbaseonly
Base phase only.
Turned off by default.
@rvindex rlcadbaseonly
@end defvr

@defvr Switch rlcadprojonly
Projection phase only.
Turned off by default.
@rvindex rlcadprojonly
@end defvr

@defvr Switch rlcadextonly
Extension phase only.
Turned off by default.
@rvindex rlcadextonly
@end defvr

@defvr Switch rlcadpartial
Partial CAD.
This is turned on by default.
@rvindex rlcadpartial
@end defvr

@defvr Switch rlcadte
Trial evaluation, the first improvement to partial CAD.
This is turned on by default.
@rvindex rlcadte
@end defvr

@defvr Switch rlcadpbfvs
Propagation below free variable space, the second improvement to partial CAD.
This is turned on by default.
@rvindex rlcadte
@end defvr

@defvr {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).
@rvindex rlcadfulldimonly
@end defvr

@defvr 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.
@rvindex rlcadtrimtree
@end defvr

@defvr {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 @code{rldnf}.
@rvindex rlcadrawformula
@end defvr

@defvr {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.
@rvindex rlcadisoallroots
@end defvr

@defvr {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 @code{rldnf}.
@rvindex rlcadrawformula
@end defvr

@defvr {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.
@rvindex rlcadisoallroots
@end defvr

@defvr {Advanced Switch} rlcadaproj
@defvrx {Advanced Switch} rlcadaprojalways
Augmented projection (always). By default, @code{rlcadaproj} is turned
on and @code{rlcadaprojalways} is turned off. If @code{rlcadaproj} is
turned off, no augmented projection is performed. Otherwerwise, if
turned on, augmented projection is performed always (if
@code{rlcadaprojalways} is turned on) or just for the free variable
space (@code{rlcadaprojalways} turned off).
@rvindex rlcadaproj
@rvindex rlcadaprojalways
@end defvr

@defvr Switch rlcadhongproj
Hong projection.
This is on by default.
If turned on, Hong's improvement for the projection operator is used.
@rvindex rlcadhongproj
@end defvr

@defvr Switch rlcadverbose
Verbose.
This is off by default.
With @code{rladverbose} on, additional verbose information is displayed.
@rvindex rlcadverbose
@end defvr

@defvr Switch rlcaddebug
Debug.
This is turned off by default.
Performes a self-test at several places, if turned on.
@rvindex rlcaddebug
@end defvr

@defvr {Advanced Switch} rlanuexverbose
Verbose.
This is off by default.
With @code{ranuexverbose} on, additional verbose information is displayed.
Not of much importance any more.
@rvindex rlanuexverbose
@end defvr

@defvr {Advanced Switch} rlanuexdifferentroots
Different roots. Unused for the moment and maybe redundant soon.
@rvindex rlanuexdifferentroots
@end defvr

@defvr Switch rlanuexdebug
Debug. This is off by default.
Performes a self-test at several places, if turned on.
@rvindex rlanuexdebug
@end defvr

@defvr Switch rlanuexpsremseq
Pseudo remainder sequences.
This is turned off by default.
This switch decides, whether division or pseudo division is used for sturm chains.
@rvindex rlanuexpsremseq
@end defvr

@defvr {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.
@rvindex rlanuexgcdnormalize
@end defvr

@defvr {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.
@rvindex rlanuexsgnopt
@end defvr

@subsection Hermitian Quantifier Elimination
@cindex Hermitian quantifier elimination

@defun rlhqe formula
@cindex quantifier elimination
@cindex Hermitian quantifier elimination
Hermitian quantifier elimination. Returns a quantifier-free
equivalent of @var{formula}. Works only in context @sc{ofsf}. There are
no degree restrictions on @var{formula}.
@rvindex rlhqe
@end defun

@node Generic Quantifier Elimination
@section Generic Quantifier Elimination

The following variant of @code{rlqe}
@rfindex rlqe
(@pxref{Quantifier Elimination}) enlarges the theory by inequalities,
i.e., @code{<>}-atomic formulas, wherever this supports the quantifier
elimination process. For geometric problems,
@cindex geometric problem
it has turned out that in most cases the additional assumptions made are
actually geometric @emph{non-degeneracy conditions}.
@cindex non-degeneracy conditions
The method has been described in detail in
@ifinfo
@ref{References,[DSW98]}.
@end ifinfo
@iftex
[DSW98].
@end iftex
It has also turned out useful for physical problems
@cindex physical problems
such as network
@ifinfo
analysis, see @ref{References,[Stu97]}.
@end ifinfo
@iftex
analysis [Stu97].
@cindex network analysis
@end iftex

@defun rlgqe formula [@var{theory} [@var{exceptionlist}]]
@rtindex theory
@cindex geometric problem
@cindex generic quantifier elimination
Generic quantifier elimination. @code{rlgqe} is not available in
@sc{acfsf}
@cindex @sc{acfsf}
and @sc{dvfsf}.
@cindex @sc{dvfsf}
@var{exceptionlist} is a list of variables empty by default. Returns a
list @code{@{th,f@}} such that @code{th} is a superset of @var{theory}
adding only inequalities, and @code{f} is a quantifier-free formula
equivalent to @var{formula} assuming @code{th}. The added inequalities
contain neither bound variables nor variables from @var{exceptionlist}.
For restrictions and options, compare @code{rlqe} (@pxref{Quantifier
Elimination}).
@end defun

@defun rlgqea formula [@var{theory} [@var{exceptionlist}]]
@rtindex theory
@cindex geometric problem
@cindex generic quantifier elimination
@cindex answer
Generic quantifier elimination with answer. @code{rlgqea} is not
available in @sc{acfsf}
@cindex @sc{acfsf}
and @sc{dvfsf}.
@cindex @sc{dvfsf}
@var{exceptionlist} is a list of variables empty by default. Returns a
list consisting of an extended theory
@cindex theory
@cindex extend theory
and an @var{elimination_answer}.
@rtindex elimination_answer
Compare @code{rlqea}/@code{rlgqe}
(@pxref{Quantifier Elimination}).
@end defun

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 @code{rlgentheo}
@rfindex rlgentheo
simplifies a formula by making further assumptions.

@defun rlgentheo theory formula [@var{exceptionlist}]
@rtindex theory
@cindex simplification
@cindex generic quantifier elimination
@cindex generate theory
Generate theory. @code{rlgentheo} is not available in @sc{dvfsf}.
@cindex @sc{dvfsf}
@var{formula} is a quantifier-free formula; @var{exceptionlist} is a
list of variables empty by default. @code{rlgentheo} extends
@var{theory}
@cindex extend theory
with inequalities not containing any variables from @var{exceptionlist}
as long as the simplification result is better wrt.@: this extended
theory. Returns a list @code{@{}extended @var{theory}, simplified
@var{formula}@code{@}}.
@end defun

@defvr Switch rlqegenct
@cindex generate theory
@cindex complexity of terms
Quantifier elimination generate complex theory.
@cindex complex theory
This is on by default, which allows @code{rlgentheo}
@rfindex rlgentheo
to assume inequalities over non-monomial terms with the
generic quantifier elimination.
@end defvr

@defun rlgcad formula
@rtindex theory
@cindex generic cylindrical algebraic decomposition
Generic cylindrical algebraic decomposition. @code{rlgcad} is
available only for @sc{ofsf}.
Compare @code{rlcad} (@pxref{Quantifier
Elimination}) and @code{rlgqe} (@pxref{Generic Quantifier
Elimination}).
@end defun

@defun rlghqe formula
@rtindex theory
@cindex generic Hermitian quantifier elimination
Generic Hermitian quantifier elimination. @code{rlghqe} is
available only for @sc{ofsf}.
Compare @code{rlhqe} (@pxref{Quantifier
Elimination}) and  @code{rlgqe} (@pxref{Generic Quantifier
Elimination}).
@end defun


@node Local Quantifier Elimination
@section Local Quantifier Elimination

In contrast to the generic quantifier elimination
@rfindex rlgqe
(@pxref{Generic Quantifier Elimination})
the following variant of @code{rlqe}
@rfindex rlqe
(@pxref{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
@ifinfo
@ref{References,[DW00]}.
@end ifinfo
@iftex
[DW00].
@end iftex

@defun rllqe formula @var{theory} @var{suggestedpoint}
@rtindex theory
@cindex local quantifier elimination
Local quantifier elimination. @code{rllqe} is not available in
@sc{acfsf}
@cindex @sc{acfsf}
and @sc{dvfsf}.
@cindex @sc{dvfsf}
@var{suggestedpoint} is a list of equations @code{var=value} where
@code{var} is a free variable and @code{value} is a rational number.
Returns a list @code{@{th,f@}} such that @code{th} is a superset of
@var{theory}, and @code{f} is a quantifier-free formula equivalent to
@var{formula} assuming @code{th}. The added inequalities contains
exclusively variables occuring on the left hand sides of equiations in
@var{suggestedpoint}. For restrictions and options, compare @code{rlqe}
(@pxref{Quantifier Elimination}).
@end defun

@node Linear Optimization
@section Linear Optimization

In the context @sc{ofsf},
@cindex @sc{ofsf}
there is a linear optimization method implemented, which uses quantifier
elimination
@cindex quantifier elimination
(@pxref{Quantifier Elimination}) encoding the target function by an
additional constraint
@cindex constraint
including a dummy variable. This optimization
technique has been described in
@ifinfo
@ref{References,[Wei94a]}.
@end ifinfo
@iftex
[Wei94a].
@end iftex

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

@defvr Switch rlopt1s
@cindex optimization
@cindex linear optimization
@cindex solution
Optimization one solution. This is off by default. @code{rlopt1s} is
relevant only for @sc{ofsf}.
@cindex @sc{ofsf}
If on, @code{rlopt}
@rfindex rlopt
returns at most one solution point.
@end defvr

@node References
@chapter References
Most of the references listed here are available on

@center @t{http://www.fmi.uni-passau.de/~redlog/}.

@table @asis

@item [CH91]
George E. Collins and Hoon Hong. Partial cylindrical algebraic decomposition
for quantifier elimination. @cite{Journal of Symbolic
Computation}, 12(3):299-328, September 1991.

@item [Dol99]
Andreas Dolzmann. Solving Geometric Problems with Real Quantifier
Elimination. Technical Report MIP-9903, FMI, Universitaet Passau,
D-94030 Passau, Germany, January 1999.

@item [DGS98]
Andreas Dolzmann, Oliver Gloor, and Thomas Sturm. Approaches to parallel
quantifier elimination. In Oliver Gloor, editor, @cite{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.

@item [DS97]
Andreas Dolzmann and Thomas Sturm. Simplification of quantifier-free
formulae over ordered fields. @cite{Journal of Symbolic Computation},
24(2):209-231, August 1997.

@item [DS97a]
Andreas Dolzmann and Thomas Sturm. Redlog: Computer algebra meets computer
logic. @cite{ACM SIGSAM Bulletin}, 31(2):2--9, June 1997.

@item [DS97b]
Andreas Dolzmann and Thomas Sturm. Guarded expressions in practice. In
Wolfgang W. Kuechlin, editor, @cite{Proceedings of the 1997
International Symposium on Symbolic and Algebraic Computation (ISSAC
97)}, pages 376--383, New York, July 1997. ACM, ACM Press.

@item [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.

@item [DSW98]
Andreas Dolzmann, Thomas Sturm, and Volker Weispfenning. A new approach
for automatic theorem proving in real geometry. @cite{Journal of
Automated Reasoning}, 21(3):357-380, December 1998.

@item [DSW98a]
Andreas Dolzmann, Thomas Sturm, and Volker Weispfenning. Real quantifier
elimination in practice. In B. H. Matzat, G.-M. Greuel, and G. Hiss,
editors, @cite{Algorithmic Algebra and Number Theory}, pages 221-248.
Springer, Berlin, 1998.

@item [DW00]
Andreas Dolzmann and Volker Weispfenning. Local Quantifier Elimination.
In Carlo Traverso, editor, @cite{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.

@item [LW93]
Ruediger Loos and Volker Weispfenning. Applying linear quantifier
elimination. @cite{The Computer Journal}, 36(5):450--462, 1993. Special
issue on computational quantifier elimination.

@item [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.

@item [Stu00]
Thomas Sturm. Linear problems in valued fields. @cite{Journal of Symbolic
Computation}, 30(2):207-219, August 2000.

@item [SW97a]
Thomas Sturm and Volker Weispfenning. Rounding and blending of solids by
a real elimination method. In Achim Sydow, editor, @cite{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.

@item [SW98]
Thomas Sturm and Volker Weispfenning. Computational geometry problems in
Redlog. In Dongming Wang, editor, @cite{Automated Deduction in
Geometry}, volume 1360 of Lecture Notes in Artificial Intelligence
(Subseries of LNCS), pages 58-86, Springer-Verlag Berlin Heidelberg,
1998.

@item [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.

@item [Wei88]
Volker Weispfenning. The complexity of linear problems in fields.
@cite{Journal of Symbolic Computation}, 5(1):3--27, February, 1988.

@item [Wei92]
Volker Weispfenning. Comprehensive Groebner Bases.
@cite{Journal of Symbolic Computation}, 14:1--29, July, 1992.

@item [Wei94a]
Volker Weispfenning. Parametric linear and quadratic optimization by
elimination. Technical Report MIP-9404, FMI, Universitaet Passau,
D-94030 Passau, Germany, April 1994.

@item [Wei94b]
Volker Weispfenning. Quantifier elimination for real algebra---the cubic
case. In @cite{Proceedings of the International Symposium on Symbolic
and Algebraic Computation in Oxford}, pages 258--263, New York, July
1994. ACM Press.

@item [Wei95]
Volker Weispfenning. Solving parametric polynomial equations and
inequalities by symbolic algorithms. In J. Fleischer et al., editors,
@cite{Computer Algebra in Science and Engineering}, pages 163-179, World
Scientific, Singapore, 1995.

@item [Wei97]
Volker Weispfenning. Quantifier elimination for real algebra---the
quadratic case and beyond. @cite{Applicable Algebra in Engineering
Communication and Computing}, 8(2):85-101, February 1997.

@item [Wei97a]
Volker Weispfenning. Simulation and optimization by quantifier
elimination. @cite{Journal of Symbolic Computation}, 24(2):189-208, August
1997.

@item [Wei90]
Volker Weispfenning. The complexity of almost linear diophantine problems.
@cite{Journal of Symbolic Computation}, 10(5):395-403, November 1990.

@end table

@node Functions
@unnumbered Functions

@menu
* Documentation of Functions::
* References to Functions::
@end menu

@node Documentation of Functions
@unnumberedsec Documentation of Functions
@printindex fn

@node References to Functions
@unnumberedsec References to Functions
@printindex rf

@node Switches and Variables
@unnumbered Switches and Variables

@menu
* Documentation of Switches and Variables::
* References to Switches and Variables::
@end menu

@node Documentation of Switches and Variables
@unnumberedsec Documentation of Switches and Variables
@printindex vr
@page

@node References to Switches and Variables
@unnumberedsec References to Switches and Variables
@printindex rv

@node Data Structures
@unnumbered Data Structures

@menu
* Documentation of Data Structures::
* References to Data Structures::
@end menu

@node Documentation of Data Structures
@unnumberedsec Documentation of Data Structures
@printindex tp

@node References to Data Structures
@unnumberedsec References to Data Structures
@printindex rt

@node Index
@unnumbered Index
@printindex cp

@shortcontents
@contents
@bye