Cylindrical Algebraic Decomposition

A={x^2+y^2-4,(x-1)(y-1)-1};

Deg[p_,x_]:=Exponent[p,x];
LC[p_,x_]:=Coefficient[p,x,Deg[p,x]]

PFS=Union[LC[A,y],Discriminant[A,y],{Resultant[A[[1]],A[[2]],y]}]//Factor

CAD=Union[A,PFS]

ContourPlot[CAD==0,{x,-5,5},{y,-5,5}]

PFS=Union[LC[A,x],Discriminant[A,x],{Resultant[A[[1]],A[[2]],x]}]//Factor

CADx=Union[A,PFS]

ContourPlot[CADx==0,{x,-5,5},{y,-5,5}]

Example : unit ball 3D

A3={x^2+y^2+z^2-1};
A2 = Union[LC[A3,z],Discriminant[A3,z]]

A1=Union[LC[A2,y],Discriminant[A2,y]]

A=Union[A1,A2,A3];
ContourPlot3D[A==0,{x,-2,2},{y,-2,2},{z,-2,2}]

Example : tacnode

A={2x^4-3x^2y+y^4-2y^3+y^2}

A1=Union[LC[A,y],Discriminant[A,y]]

A2 = Union[A,A1]

ContourPlot[A2==0,{x,-2,2},{y,-1,3},PlotPoints->500]

A1x=Union[LC[A,x],Discriminant[A,x]]

A2x=Union[A,A1x]//Factor

A2x1={2,2 (x^4)-3 (x^2) y+(y^2)-2 (y^3)+(y^4), (((-1+y))^2) ,(y^6), (((-1-16 y+8 (y^2)))^2)}

{2,2 (x^4)-3 (x^2) y+(y^2)-2 (y^3)+(y^4),(((-1+y))^2),(y^6),(((-1-16 y+8 (y^2)))^2)}

ContourPlot[A2x1==0,{x,-2,2},{y,-1,3},PlotPoints->500]

?CylindricalDecomposition

A={x^2+y^2-4,(x-1)(y-1)-1};

CylindricalDecomposition[A[[1]]>0 && A[[2]]>0,{x,y}]

CylindricalDecomposition[A[[1]]>0 && A[[2]]>0,{y,x}]

RegionPlot[%30,{x,-3,3},{y,-3,3}]

CylindricalDecomposition[(A[[1]]>0 && A[[2]]>0)||(A[[1]]<=0 && A[[2]]<=0),{x,y}]

RegionPlot[%32,{x,-3,3},{y,-3,3}]

CylindricalDecomposition[ForAll[x,Exists[y,(A[[1]]>0 && A[[2]]>0)||(A[[1]]<=0 && A[[2]]<=0)]],{}]

?Reduce

?Resolve

Resolve[ForAll[x,Exists[y,(A[[1]]>0 && A[[2]]>0)||(A[[1]]<=0 && A[[2]]<=0)]],{}]

Resolve[Exists[y,(A[[1]]>0 && A[[2]]>0)||(A[[1]]<=0 && A[[2]]<=0)],{x}]

?GenericCylindricalDecomposition

{cad,hypersurfaces}=GenericCylindricalDecomposition[(A[[1]]>0 && A[[2]]>0)||(A[[1]]<=0 && A[[2]]<=0),{x,y}];

cad

hypersurfaces

<<RISC`SumCracker`

SumCracker Package version 0.11
written by Manuel Kauers
Copyright Research Institute for Symbolic Computation (RISC),
Johannes Kepler University, Linz, Austria

ProveInequality[LegendreP[n+1,x]^2-LegendreP[n,x] LegendreP[n+2,x]>=0,Using->{-1<=x<=1},Variable->n]

ProveInequality[LegendreP[n+1,x]^2-LegendreP[n,x] LegendreP[n+2,x]>=0,Using->{-1<=x<=1},Variable->n,Infolevel->3]

ProveInequality[...,Where->{recursive definition}, Using->{-1<x<1},...

ProveInequality[3^n>=2^n,Infolevel->3]

ProveInequality[LegendreP[n+1,x]^2-x LegendreP[n,x] LegendreP[n+2,x]>=0,Using->{0<x<1},Variable->n,From->1,Infolevel->2]