qepmax package

Qepmax is a Qepcad B - Maxima interfacing module written in
Maxima language and Common Lisp. As Qepcad B provides so 
called quantifier elimination in the real domain, Qepmax
adds this functionality to Maxima computer algebra system.

Installation instructions are in the file INSTALL.
Lincese terms can be found in each source files. 
qepmax package is in GPL v2.

Qepmax package is written by Yasuaki Honda, then Prof. 
Dr. Reinhard Oldenburg of Goethe-Universität Frankfurt has
contributed the improvements for allowing the use of logical 
operators and rational functions as well as better function
interface.

Further, ehito san has contributed the improvement of the
treatment of rational functions.

This file introduces you what is qepcad and what 
you can do with it using qepmax package.

- What is Quantifier Elimination?

- What does Qepcad B do?

- What is qepmax package and how to use it?




- What is Quantifier Elimination?
A large size of problems can be expressed as a first order
predicate logic with the following properties:
* variables are in real number domain
* predicates are =, <, >, <=, >=, #(not equal)
* terms are polinomials (or rational functions)

A logical formula with some of its variables quntified is 
called a Talski sentence. 
Example: a circle x^2+y^2=1 and a line y=x/2+1/3 crosses with 
each other.
E x, E y, x^2+y^2=1 and y=x/2+1/3

The quntifier elimination is a technique to obtain the
equivarent condition to the given Talski sentence. The
resulted condition does not contain any quantified variables.

By using the quantifier elimination technique, we can obtain 
an equivarent condition:
true

On the other hand, from
E x, E y, x^2+y^2=1 and y=x/2+5
we will obtain
false
since there is no such x and y.

Further more, considering the following Talski sentence with free variable a:
E x, E y, x^2+y^2=1 and y=x/2+a

Using the quantifier elimination, we obtain a condition on m:
4*a^2-5<=0

So, while a is in this range, the circle and the line cross, but
they don't cross if a is not in the range above.


- What does Qepcad B do?
Qepcad B is a software that implements a quantifier elimination
algorithm called Cylindrical Algebraic Decomposition (CAD).
The software is developed by Chris Brown of US Naval Academy.
The homepage of the software is:
http://www.usna.edu/CS/~qepcad/B/QEPCAD.html

On starting the program Qepcad B, the interactive session starts.
You give a list of variables, number of free variables,
a list of quntified variables, and a Talski sentence with Qepcad B 
syntax during the session. Alternatively, you can supply all
such information in a file and Qepcad B processes it.
Then the program computes the equivarent condition to the
specified Talski sentence, only including the free variables. 

It is a fun to use Qepcad B directly from its command line 
interface, as it provides many commands and options to use
during the interactive sessions. 

- What is qepmax package and how to use it?
qepmax is a Maxima package that calls Qepcad B internally using
sysmtem() function to process Talski sentence represented using
Maxima syntax.

Assuming it is correctly installed according to INSTALL, you
can load the package by:
(%i1) load(qepmax);

Qepmax package provides a function qe(QFList, aLogicalExp).
QFList is a list of quantified variables. aLogicalExp is a
expression in the real domain. You can use =,<,>,<=,>=,# as
the predicates, polynomials and rational functions as terms,
and %and, %or, %not, %implies as the logical operators.
In polimomials and rational functions, you can use rational
numbers and variables as coefficients.

Let's use the above examples to see how to use qe().

(%i3) qe([[E,x],[E,y]], x^2+y^2=1 %and y=x/2+1/3);
(%o3) true

The return value true indicates that this Talski sentence
is equivarent to true, meaning that the circle and the line
crosses.

(%i4) qe([[E,x],[E,y]], x^2+y^2=1 %and y=x/2+5);
(%o4) false
This means this Talski sentence is equivarent to false. The
circle and the line does not cross.

The natural question is: when the circle and the line
cross? You can express the line with a parameter 'a', like:
y=x/2+a
and you can use quantifier elimination to find the condition
of 'a':
(%i5) qe([[E,x],[E,y]], x^2+y^2=1 %and y=x/2+a);
(%o5) 4*a^2-5 <= 0
This is the same -sqrt(5/4)<=a<=sqrt(5/4). If a is in this range,
the circle and the line cross. Otherwise, they don't.

Rather time consuming example:
Find max and min of x*y*z when x,y,z satisfies x^2+y^2+z^2=6 and
x+y+z=4:
qe([[E,x],[E,y],[E,z]],x^2+y^2+z^2=6 %and x+y+z=4 %and v=x*y*z);


You can see other examples in rtest_qepmax.mac file.

Yasuaki Honda, Chiba, Japan