Home Online Manual
Top
Back: intersectpar
Forward: inout_lib
FastBack:
FastForward:
Up: grobcov_lib
Top: Singular Manual
Contents: Table of Contents
Index: Index
About: About this document

D.2.4.22 ADGT

Procedure from library grobcov.lib (see grobcov_lib).

Usage:
ADGT(ideal H, ideal T, ideal H1,ideal T1[,options]);
H: ideal in Q[a][x] hypothesis
T: ideal in Q[a][x] thesis
H1: ideal in Q[a][x] negative hypothesis, only dependent on [a] T1: ideal in Q[a][x] negative thesis
of the Proposition (H and not H1) => (T and not T1)

Return:
The list [[1,S1],[2,S2],..],
S1, S2, .. represent the set of parameter values
that must be verified as supplementary
conditions for the Proposition to become a Theorem.
They are given by default in Prep.
If the proposition is generally true,
(the proposition is already a theorem), then
the generic segment of the internal grobcov
called is also returned to provide information
about the values of the variables determined
for every value of the parameters.

Options:
An option is a pair of arguments: string,
integer. To modify the default options, pairs
of arguments -option name, value- of valid options
must be added to the call.
Option "rep",0-1: The default is ("rep",0)
and then the segments are given in canonical
P-representation.
Option ("rep",1) represents the segments
in canonical C-representation,
Option "gseg",0-1: The default is "gseg",1
and then when the proposition is generally true,
ADGT outputs a second element which is the
"generic segment" to provide supplementary information. With option "gseg",0 this is avoided.

Note:
The basering R, must be of the form Q[a][x],
(a=parameters, x=variables), and
should be defined previously. The ideals
must be defined on R.

Example:
 
LIB "grobcov.lib";
// Determine the supplementary conditions
// for the non-degenerate  triangle A(-1,0), B(1,0), C(x,y)
// to have an ortic non-degenerate isosceles triangle
if(defined(R)){kill R;}
ring R=(0,x,y),(x2,y2,x1,y1),lp;
// Hypothesis H
ideal H=-y*x1+(x-1)*y1+y,
(x-1)*(x1+1)+y*y1,
-y*x2+(x+1)*y2-y,
(x+1)*(x2-1)+y*y2;
// Thesis T
ideal T=(x1-x)^2+y1^2-(x2-x)^2-y2^2;
// Negative Hypothesis H1
ideal H1=y;
// Negative Thesis T1
ideal T1=x*(y1-y2)-y*(x1-x2)+x1*y2-x2*y1;
// Complementary conditions for the
// Proposition (H and not H1) => (T and not T1)
// to be true
ADGT(H,T,H1,T1);
==> [1]:
==>    [1]:
==>       1
==>    [2]:
==>       [1]:
==>          [1]:
==>             _[1]=(x^2-y^2-1)
==>          [2]:
==>             [1]:
==>                _[1]=(y)
==>                _[2]=(x-1)
==>             [2]:
==>                _[1]=(y)
==>                _[2]=(x+1)
==>             [3]:
==>                _[1]=(y^2+1)
==>                _[2]=(x)
==>       [2]:
==>          [1]:
==>             _[1]=(x)
==>          [2]:
==>             [1]:
==>                _[1]=(y-1)
==>                _[2]=(x)
==>             [2]:
==>                _[1]=(y)
==>                _[2]=(x)
==>             [3]:
==>                _[1]=(y^2+1)
==>                _[2]=(x)
==>             [4]:
==>                _[1]=(y+1)
==>                _[2]=(x)
//********************************************
// Example of automatic demonstrations of a theorem
// The Nine Points Circle Theorem:
if(defined(R1)){kill R1;}
ring R1=(0,x,y),(x1,y1,x2,y2,yh,a,b,r),dp;
short=0;
//Hypothesis H
ideal H=y*x1+y1-x*y1-y,
(x-1)*(x1+1)+y*y1,
-y*x2+y2+x*y2-y,
(x+1)*(x2-1)+y*y2,
(x1-a)^2+(y1-b)^2-r^2,
(x2-a)^2+(y2-b)^2-r^2,
(x-a)^2+b^2-r^2,
-yh+x*y1-x1*yh+y1;
// Thesis T
ideal T=yh+x*y2-x2*yh-y2,
(x-1-2*a)^2+(yh-2*b)^2-4*r^2,
(x+1-2*a)^2+(yh-2*b)^2-4*r^2,
4*(x-a)^2+(y+yh-2*b)^2-4*r^2,
(x-1-2*a)^2+(y-2*b)^2-4*r^2,
(x+1-2*a)^2+(y-2*b)^2-4*r^2,
4*(x-a)^2+(yh+y-2*b)^2-4*r^2;
ADGT(H,T,y,1);
==> [1]:
==>    [1]:
==>       1
==>    [2]:
==>       [1]:
==>          [1]:
==>             _[1]=0
==>          [2]:
==>             [1]:
==>                _[1]=(x^2-2*x+y^2+1)
==>             [2]:
==>                _[1]=(x^2+2*x+y^2+1)
==>             [3]:
==>                _[1]=(y)
==> [2]:
==>    [1]:
==>       Generic segment
==>    [2]:
==>       [1]:
==>          _[1]=b
==>          _[2]=a
==>          _[3]=yh
==>          _[4]=y2
==>          _[5]=x2
==>          _[6]=y1
==>          _[7]=x1
==>          _[8]=r^2
==>       [2]:
==>          _[1]=(4*y)*b+(x^2-y^2-1)
==>          _[2]=2*a+(-x)
==>          _[3]=(y)*yh+(x^2-1)
==>          _[4]=(x^2+2*x+y^2+1)*y2+(-2*x*y-2*y)
==>          _[5]=(x^2+2*x+y^2+1)*x2+(-x^2-2*x+y^2-1)
==>          _[6]=(x^2-2*x+y^2+1)*y1+(2*x*y-2*y)
==>          _[7]=(x^2-2*x+y^2+1)*x1+(x^2-2*x-y^2+1)
==>          _[8]=(16*y^2)*r^2+(-x^4-2*x^2*y^2+2*x^2-y^4-2*y^2-1)
==>       [3]:
==>          [1]:
==>             [1]:
==>                _[1]=0
==>             [2]:
==>                [1]:
==>                   _[1]=(x^2-2*x+y^2+1)
==>                [2]:
==>                   _[1]=(x^2+2*x+y^2+1)
==>                [3]:
==>                   _[1]=(y)
// Thus the theorem is true.