1on rlverbose; 2 3% Ordered fields standard form: 4rlset ofsf; 5rlset(); 6 7% Chains 8-3/5<x>y>z<=a<>b>c<5/3; 9 10% For-loop actions. 11g := for i:=1:6 mkor 12 for j := 1:6 mkand 13 mkid(a,i) <= mkid(a,j); 14 15% Quantifier elimination and variants 16h := rlsimpl rlall g; 17rlmatrix h; 18on rlrealtime; 19rlqe h; 20off rlrealtime; 21 22h := rlsimpl rlall(g,{a2}); 23rlqe h; 24 25off rlqeheu,rlqedfs; 26rlqe ex(x,a*x**2+b*x+c>0); 27on rlqedfs; 28rlqe ex(x,a*x**2+b*x+c>0); 29on rlqeheu; 30 31rlqe(ex(x,a*x**2+b*x+c>0),{a<0}); 32 33rlgqe ex(x,a*x**2+b*x+c>0); 34rlthsimpl ({a*b*c=0,b<>0}); 35 36 37rlqe ex({x,y},(for i:=1:5 product mkid(a,i)*x**10-mkid(b,i)*y**2)<=0); 38 39sol := rlqe ex(x,a1*a2*x**2+b*x+c>0); 40rlatnum sol; 41rldepth sol; 42 43rlatl sol; 44rlatml sol; 45rlterml sol; 46rltermml sol; 47rlifacl sol; 48rlifacml sol; 49 50rlstruct(sol, fac=no, w); 51rlstruct(sol); 52 53rltab sol; 54rlatnum ws; 55rlgsn sol; 56rlatnum ws; 57 58off rlverbose; 59 60rlqea ex(x,m*x+b=0); 61 62% Substitution 63sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x>a)); 64 65% Boolean normal forms. 66f1 := x=0 and b>=0; 67f2 := a=0; 68f := f1 or f2; 69 70rlcnf f; 71 72rldnf ws; 73 74rlcnf f; 75 76% Negation normal form and prenex normal form 77hugo := a=0 and b=0 and y<0 equiv ex(y,y>=a) or a>0; 78rlnnf hugo; 79rlpnf hugo; 80 81% Length and Part 82part(hugo,0); 83part(hugo,2,1,2); 84length ws; 85length hugo; 86length part(hugo,1); 87 88% Tableau 89mats := all(t,ex({l,u},( 90(t>=0 and t<=1) impl 91(l>0 and u<=1 and 92 -t*x1+t*x2+2*t*x1*u+u=l*x1 and 93 -2*t*x2+t*x2*u=l*x2)))); 94sol := rlgsn rlqe mats; 95rltab(sol,{x1>0,x1<0,x1=0}); 96 97% Part on psopfn / cleanupfn 98part(rlqe ex(x,m*x+b=0),1); 99walter := (x>0 and y>0); 100rlsimpl(true,rlatl walter); 101part(rlatl walter,1,1); 102 103% QE by partial CAD: 104cox6 := ex({u,v},x=u*v and y=u**2 and z=v**2)$ 105rlcad cox6; 106 107% Generate Theory 108rlgentheo({a=0}, a*x+b<>0); 109 110% Algebraically closed fields standard form: 111sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x<>a)); 112 113rlset acfsf; 114 115rlsimpl(x^2+y^2+1<>0); 116 117rlqe ex(x,x^2=y); 118 119clear f; 120h := rlqe ex(x,x^3+a*x^2+b*x+c=0 and x^3+d*x^2+e*x+f=0); 121rlstruct h; 122rlqe rlall (h equiv resultant(x^3+a*x^2+b*x+c,x^3+d*x^2+e*x+f,x)=0); 123clear h; 124 125% Discretely valued fields standard form: 126rlset dvfsf; 127sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x~a)); 128 129% P-adic Balls, taken from Andreas Dolzmann, Thomas Sturm. P-adic 130% Constraint Solving, Proceedings of the ISSAC '99. 131rlset dvfsf; 132rlqe all(r_1,all(r_2,all(a,all(b, 133ex(x,r_1||x-a and r_2||x-b and r_1|r_2) impl 134all(y,r_2||y-b impl r_1||y-a))))); 135rlmkcanonic ws; 136rlset(dvfsf,100003); 137rlqe all(r_1,all(r_2,all(a,all(b, 138ex(x,r_1||x-a and r_2||x-b and r_1|r_2) impl 139all(y,r_2||y-b impl r_1||y-a))))); 140 141% Size of the Residue Field, taken from Andreas Dolzmann, Thomas 142% Sturm. P-adic Constraint Solving. Proceedings of the ISSAC '99. 143rlset(dvfsf); 144rlqe ex(x,x~1 and x-1~1 and x-2~1 and x-3~1 and 2~1 and 3~1); 145rlexplats ws; 146rldnf ws; 147 148% Differentially closed fields standard form: 149rlset dcfsf; 150sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,d(x, 4) <> a)); 151 152% An Example on Differential Algebras by E. Pankratiev taken from A. Dolzmann, 153% T. Sturm. Generalized Constraint Solving over Differential Algebras. 154% Proceedings of the CASC 2004. 155pankratiev := all(x,d(x, 1)**2 + x = 0 impl (d(x, 1) = a or d(x, 2) = b)); 156rlqe pankratiev; 157 158% Selecting contexts: 159 160rlset acfsf; 161f:= ex(x,m*x+b=0); 162rlqe f; 163rlset dcfsf; 164rlqe f; 165rlset dvfsf; 166rlqe f; 167rlset ofsf; 168rlqe f; 169 170end; % of file 171