Algebraic Computation in Version 12

Adam strzebonski
Wolfram Research, inc.

Outline

Equation and Inequality Solving

Exact Optimization

Equation Manipulation

Equational Logic Proofs

Topological Properties of Solution Sets

Use CylindricalDecomposition to compute topological properties of solution sets of polynomial equations and inequalities:

ineq=7(x^4)≥7(x^2)+7(y^2)-1;

Compute the solution set:

cad1=CylindricalDecomposition[ineq,{x,y}]

Visualize the result:

Region`SemialgebraicRegionPlot[ImplicitRegion[cad1,{x,y}],{{-3,3},{-3,3}}]

Compute the boundary of the solution set:

cad2=CylindricalDecomposition[ineq,{x,y},"Boundary"]

Visualize the result:

Region`SemialgebraicRegionPlot[ImplicitRegion[cad2,{x,y}],{{-3,3},{-3,3}}]

Compute the connected components of the solution set:

cads=CylindricalDecomposition[ineq,{x,y},"Components"]

Visualize the result:

Show[MapThread[Region`SemialgebraicRegionPlot[ImplicitRegion[#1,{x,y}],{{-3,3},{-3,3}},"PolygonInColor"->#2,"LineInColor"->#3,"PointInColor"->#3]&,{cads,{LightRed,LightBlue,LightGreen},{Red,Blue,Green}}]]

Solving Vector and Matrix Inequalities

Find a pair of orthogonal vectors satisfying a vector inequality and a norm condition:

FindInstance[x.y==0&&-x\[VectorLess]y\[VectorLess]x&&Norm[x]==1&&(x|y)∈Vectors[2,(Reals)],{x,y}]

Visualize the solution:

{xx,yy}={x,y}/.%[[1]];vecs=Graphics[{{Red,Arrow[{{0,0},xx}]},{Blue,Arrow[{{0,0},-xx}]},{Green,Arrow[{{0,0},yy}]}}];
reg=Reduce[VectorLess[{-xx,{a,b},xx}],{a,b},Reals];
rp=RegionPlot[reg,{a,-1,1},{b,-1,1},PlotPoints->50,PlotStyle->GrayLevel[0.9],BoundaryStyle->GrayLevel[0.7]];
Show[{rp, vecs}]

Solve a system of vector inequalities:

Reduce[x\[VectorLess](x^3)&&x.x≤9&&x∈Vectors[2,(Reals)],x]

Visualize the solution set:

RegionPlot[Evaluate[%/.x->{a,b}],{a,-1.2,3.2},{b,-1.2,3.2},PlotPoints->50]

Other Improvements in Equation and Inequality Solving

Large Triangular Polynomial Systems

Shown are timings for finding the exact solutions of triangular systems of n polynomial equations in n variables. Each polynomial is dense of total degree 7 with randomly generated integer coefficients between -100 and 100. The experiment was performed on an Intel Xeon 3.07 GHz 64-bit Linux system, with a time limit of 1 hour. The number at the bottom tells how many times faster Version 12 is than Version 11.

Diophantine Equations with Irrational Coefficients

Reduce[GoldenRatio (x^2)-(Sqrt[5]) (y^2)-z==(Sqrt[5]),{x,y,z},(PositiveIntegers)]

Solve[(x^2) (π+(Sqrt[2]))+(Sqrt[6]) x y z+π (y^2)+(π^2) (Sqrt[3]) (z^2) (t^2)-3 (Sqrt[3]) z t x-(Sqrt[3]) (z^3)+63 (Sqrt[3])==(Sqrt[2 (109+12 (Sqrt[3]))])+5 π+144 (Sqrt[3]) (π^2),{x,y,z,t},(Integers)]

Inequalities Involving Transcendental Functions

Reduce[Gamma[x]≤2x&&-2≤x≤2,x,(Reals)]

Systems Involving Symbolic Derivatives

Solve[(∂_x)EllipticThetaPrime[2,x,(1/2)]==0&&0≤x<2 π,x]

Visualize the solutions:

pts={x,EllipticThetaPrime[2,x,(1/2)]}/.%;
pl=Plot[EllipticThetaPrime[2,x,(1/2)],{x,0,2Pi}];
Show[{pl,Graphics[{Red,PointSize[Large],Point[N[pts]]}]}]

Optimization of Periodic Functions

Minimize a combination of trigonometric functions with commensurable periods:

Minimize[Sin[(E^(x/3))-3 x]+2 ((Cos[2 (E^(x/3))-6 x+1])^2),x]

Visualize the solution:

min={x/.%[[2]],%[[1]]};
pl=Plot[Sin[(E^(x/3))-3 x]+2 ((Cos[2 (E^(x/3))-6 x+1])^2),{x,-10,10}];
Show[{pl,Graphics[{Red,PointSize[Medium],Point[N[min]]}]}]

Find the maximum value of a combination of periodic functions with incommensurable periods. The maximum value is not attained:

MaxValue[Sin[Sin[(Sqrt[2]) x]]+2 Cos[3 x]-Erf[2+Cos[2 (Sqrt[2]) x]],x]

Visualize the solution:

max=%;{a,b}={-50,50};
pl=Plot[Sin[Sin[(Sqrt[2]) x]]+2 Cos[3 x]-Erf[2+Cos[2 (Sqrt[2]) x]],{x,a,b}];
Show[{pl,Graphics[{Red,Line[{{a,max},{b,max}}]}]}]

Find the minimum value of a combination of periodic functions with incommensurable periods over the integers:

MinValue[((Sin[π x]+Cos[Cos[E π x]])/(Cos[(Sqrt[3]) π x]+2)),x,(Integers)]

Visualize the solution:

min=%;
Show[{ListPlot[Table[((Sin[π x]+Cos[Cos[E π x]])/(Cos[(Sqrt[3]) π x]+2)),{x,0,10000}]],Graphics[{Red,Line[{{0,min},{10000,min}}]}]}]

Vector and Matrix Optimization

Minimize a vector norm subject to dot product and vector inequality constraints:

Minimize[{Norm[x-y],y.y==1&&x.y==0&&-x\[VectorLessEqual]y\[VectorLessEqual]x&&(x|y)∈Vectors[2,(Reals)]},{x,y}]

Visualize the solution:

{xx,yy}={x,y}/.%[[2]];vecs=Graphics[{{Red,Arrow[{{0,0},xx}]},{Red,Dashed,Arrow[{{0,0},-xx}]},{Blue,Arrow[{{0,0},yy}]}}];
d=Graphics[{Green,Thick,Dashed,Line[{xx,yy}]}];
reg=Reduce[VectorLess[{-xx,{x,y},xx}],{x,y},Reals];
rp=RegionPlot[reg,{x,-1,1},{y,-1,1},PlotPoints->50,PlotStyle->GrayLevel[0.95],BoundaryStyle->GrayLevel[0.8]];
Show[{rp,vecs,d}]

Find the maximal eigenvalue of a matrix and a corresponding eigenvector:

mat={{1,2,3},{6,5,4},{9,7,8}};

Maximize[{c,mat.v==c v&&v.v>0&&v∈Vectors[3,(Reals)]},{c,v}]//RootReduce

Compare with the output of Eigensystem:

Eigensystem[mat]//RootReduce

Maximize the determinant of a positive semidefinite 3×3 matrix with trace 1:

Maximize[{Det[A],Tr[A]==1&&A(Underscript[\[VectorGreater], (SemidefiniteConeList[3])])0&&A∈Matrices[3,(Reals)]},A]

Other Improvements in Exact Optimization

Optimize Univariate Elementary Functions over the Integers

Minimize[(x^3) (E^x)+(E^(E^x)),x,(Integers)]

Maximize[{ArcTan[(x^2)-1]+((Log[x])/x),x>0},x,(Integers)]

Solve Optimization Problems Involving Transcendental Functions

Maximize[10 Sin[(x^2) (y+1)]-(y^2)+5 y,{x,y}]

Visualize the solution:

max={x,y,%[[1]]}/. %[[2]];
pl=Plot3D[10 Sin[(x^2) (y+1)]-(y^2)+5 y,{x,-2,2},{y,0,5}];
Show[{pl,Graphics3D[{Red,PointSize[Medium],Point[N[max]]}]}]

Solve Optimization Problems Involving Function Compositions

Maximize[((Log[Csc[Exp[Sin[(x^2)+1]]]])^2)+3,x]

Visualize the solution:

max={x/.%[[2]],%[[1]]};
pl=Plot[((Log[Csc[Exp[Sin[(x^2)+1]]]])^2)+3,{x,-5,5}];
Show[{pl,Graphics[{Red,PointSize[Medium],Point[N[max]]}]}]

Solving Linear Equations “by Hand”

eqn1=2x+3y==5;
eqn2=x-y==5;

Multiply both sides of the second equation by 2:

MultiplySides[eqn2,2]//Expand

Subtract the result from the first equation:

SubtractSides[eqn1,%]

Divide both sides by 5 to solve for y:

DivideSides[%,5]

Multiply both sides of the result by negative 3:

MultiplySides[%,-3]

Add the result to the first equation:

AddSides[eqn1,%]

Divide both sides by 4 to solve for x:

DivideSides[%,2]

Manipulating Inequalities

Manipulate the inequality a x+b>0:

a=.;b=.;c=.;d=.;
ineq1=a x+ b>0;

Subtract b from both sides:

SubtractSides[ineq1,b]

Divide both sides by a. Since the result depends on the sign of a, a piecewise expression is returned:

DivideSides[%,a]

If an equation is added to an inequality, the result is an inequality:

AddSides[ineq1,d+c x==0]

The equation manipulation functions reorder the sides of an inequality when necessary to combine them:

AddSides[ineq1,d+c x<0]

Applying an Arbitrary Function to Equations

The function ApplySides intelligently applies a function to all sides of an equation or inequality, avoiding the need to use abstract structural operations such as Map and Thread.

For example, ApplySides can exponentiate both sides of an equation:

ApplySides[Exp,a==b]

It can apply a function to an equality with more than two expressions:

ApplySides[Log,a==b==c]

Take the sine of both sides of an equation with a condition attached:

ApplySides[Sin, ConditionalExpression[x==(a/b), b≠0]]

Apply an arbitrary function to both sides of several inequalities inside a piecewise expression:

ApplySides[f,({{\[Piecewise], ({{x>-(b/a), a>0}, {-(b/a)>x, a<0}, {a x>-b, True}})}})]

Equational Proofs in Boolean Logic

The function FindEquationalProof can construct a proof of a theorem from a set of axioms if they are all expressed in equational form, that is, equalities between formulas built from the operators of the theory.

Use AxiomaticTheory to obtain a collection of axioms for a theory, like Boolean logic. You can specify the names of the operators and constants involved. Bound variables are represented using formal symbols like \[FormalA], \[FormalB], \[FormalC]:

Column[axioms=AxiomaticTheory[{"BooleanAxioms",<|"And"->and,"Or"->or,"Not"->not|>}]]

Construct a proof of an equation:

proof=FindEquationalProof[ForAll[{a,b},or[not[or[not[a],b]],not[or[not[a],not[b]]]]==a],axioms]

Display the proof as a graph showing the flow of lemmas proceeding from the axioms (green squares) to the conclusion (red square). Triangles and circles represent different types of lemmas:

proof["ProofGraph"]

Alternatively, display all details about the proof steps:

proof["ProofDataset"]

Textual Form of a Proof in Group Theory

Get the axioms of group theory, using as CircleTimes as the group product, (OverTilde[1]) as the identity element, and OverBar as the inverse operator. Group elements are represented by default as formal symbols \[FormalA], \[FormalB], \[FormalC]:

groupTheory=AxiomaticTheory["GroupAxioms"]

One of the axioms states existence of right identity. Prove that a right identity is also a left identity:

proof=FindEquationalProof[ForAll[x,(OverTilde[1])⊗x==x],groupTheory]

Get a human-readable form of the 11 steps of the proof:

proof["ProofNotebook"]

Summary

Version 12 of the Wolfram Language™ extends its already strong capabilities in algebraic computation with functionality for users ranging from pre-college students to researchers. Improvements span from new functions that manipulate equations step by step to more powerful equation and optimization solvers, to equational theorem proving.

Further information and examples about the new features are available here.