|
benchmarks : THEORY
BEGIN
IMPORTING strategy
x,x1,x2,x3,x4,x5,x6,x7,x8:VAR real
%|- *_ : PROOF (bernstein) QED
% Heart dipole
Heart(x1,x2,x3,x4,x5,x6,x7,x8): MACRO real =
-x1*x6^3+3*x1*x6*x7^2-x3*x7^3+3*x3*x7*x6^2-x2*x5^3+3*x2*x5*x8^2-x4*x8^3+3*x4*x8*x5^2-0.9563453
Heart_forall_: LEMMA
-0.1 <= x1 AND x1 <= 0.4 AND
0.4 <= x2 AND x2 <= 1 AND
-0.7 <= x3 AND x3 <= -0.4 AND
-0.7 <= x4 AND x4 <= 0.4 AND
0.1 <= x5 AND x5 <= 0.2 AND
-0.1 <= x6 AND x6 <= 0.2 AND
-0.3 <= x7 AND x7 <= 1.1 AND
-1.1 <= x8 AND x8 <= -0.3 IMPLIES
Heart(x1,x2,x3,x4,x5,x6,x7,x8) >= -1.7435
Heart_exists_: LEMMA
EXISTS (x1,x2,x3,x4,x5,x6,x7,x8:real):
-0.1 <= x1 AND x1 <= 0.4 AND
0.4 <= x2 AND x2 <= 1 AND
-0.7 <= x3 AND x3 <= -0.4 AND
-0.7 <= x4 AND x4 <= 0.4 AND
0.1 <= x5 AND x5 <= 0.2 AND
-0.1 <= x6 AND x6 <= 0.2 AND
-0.3 <= x7 AND x7 <= 1.1 AND
-1.1 <= x8 AND x8 <= -0.3 AND
Heart(x1,x2,x3,x4,x5,x6,x7,x8) <= -1.7434
Magnetism(x1,x2,x3,x4,x5,x6,x7): MACRO real =
x1^2+2*x2^2+2*x3^2+2*x4^2+2*x5^2+2*x6^2+2*x7^2-x1
Magnetism_forall_: LEMMA
x1<=1 AND x2<=1 AND x3<=1 AND x4<=1 AND x5<=1 AND x6<=1 AND x7<=1 AND
-1<=x1 AND -1<=x2 AND -1<=x3 AND -1<=x4 AND -1<=x5 AND -1<=x6 AND -1<=x7
IMPLIES
Magnetism(x1,x2,x3,x4,x5,x6,x7) >=-0.25001
Magnetism_exists_: LEMMA
EXISTS (x1,x2,x3,x4,x5,x6,x7):
x1<=1 AND x2<=1 AND x3<=1 AND x4<=1 AND x5<=1 AND x6<=1 AND x7<=1 AND
-1<=x1 AND -1<=x2 AND -1<=x3 AND -1<=x4 AND -1<=x5 AND -1<=x6 AND -1<=x7
AND
Magnetism(x1,x2,x3,x4,x5,x6,x7) <= -0.2499
% This answer appears to be incorrect in the paper
Butcher(x1,x2,x3,x4,x5,x6): MACRO real =
x6*x2^2 + x5*x3^2-x1*x4^2+x4^3+x4^2-(1/3)*x1+(4/3)*x4
Butcher_forall_: LEMMA
-1<=x1 AND x1<=0 AND -0.1<=x2 AND x2<=0.9 AND -0.1<=x3 AND x3<=0.5 AND
-1<=x4 AND x4<=-0.1 AND -0.1<=x5 AND x5<=-0.05 AND -0.1<=x6 AND x6<=-0.03
IMPLIES
Butcher(x1,x2,x3,x4,x5,x6) >= -1.44 %-0.21901
Butcher_exists_: LEMMA
EXISTS (x1,x2,x3,x4,x5,x6):
-1<=x1 AND x1<=0 AND -0.1<=x2 AND x2<=0.9 AnD -0.1<=x3 AND x3<=0.5 AND
-1<=x4 AND x4<=-0.1 AND -0.1<=x5 AND x5<=-0.05 AND -0.1<=x6 AND x6<=-0.03 AND
Butcher(x1,x2,x3,x4,x5,x6) <= -0.21899
Trid(x1,x2,x3,x4): MACRO real =
(x1-1)^2 + (x2-1)^2 + (x3-1)^2 + (x4-1)^2 -x1*x2-x2*x3-x3*x4
Trid_forall_: LEMMA
-16<=x1 AND x1<=16 AND -16<=x2 AND x2<=16 AND -16<=x3 AND x3<=16 AND -16<=x4 AND x4<=16 IMPLIES
Trid(x1,x2,x3,x4) >= -16.001
Trid_exists_: LEMMA
EXISTS (x1,x2,x3,x4):
-16<=x1 AND x1<=16 AND -16<=x2 AND x2<=16 AND -16<=x3 AND x3<=16 AND -16<=x4 AND x4<=16 AND
Trid(x1,x2,x3,x4) < -15.999
AdaptiveLV(x1,x2,x3,x4): MACRO real =
x1*x2^2+x1*x3^2+x1*x4^2-1.1*x1+1
AdaptiveLV_forall_: LEMMA
-2<=x1 AND x1<=2 AND -2<=x2 AND x2<=2 AND -2<=x3 AND x3<=2 AND -2<=x4 AND x4<=2 IMPLIES
AdaptiveLV(x1,x2,x3,x4) >= -20.801
AdaptiveLV_exists_: LEMMA
EXISTS (x1,x2,x3,x4):
-2<=x1 AND x1<=2 AND -2<=x2 AND x2<=2 AND -2<=x3 AND x3<=2 AND
-2<=x4 AND x4<=2 AND
AdaptiveLV(x1,x2,x3,x4) <= -20.799
Caprasse(x1,x2,x3,x4): MACRO real =
-x1*x3^3+4*x2*x3^2*x4+4*x1*x3*x4^2+2*x2*x4^3+4*x1*x3+4*x3^2-10*x2*x4-10*x4^2+2
Caprasse_forall_: LEMMA
-0.5<=x1 AND x1<=0.5 AND -0.5<=x2 AND x2<=0.5 AND -0.5<=x3 AND
x3<=0.5 AND -0.5<=x4 AND x4<=0.5 IMPLIES
Caprasse(x1,x2,x3,x4) >= -3.18010
Caprasse_exists_: LEMMA
EXISTS (x1,x2,x3,x4):
-2<=x1 AND x1<=2 AND -2<=x2 AND x2<=2 AND -2<=x3 AND x3<=2 AND -2<=x4 AND x4<=2 AND
Caprasse(x1,x2,x3,x4) <= -3.18009
% The answer in the paper for the Schwefel function is also incorrect. It is actually zero.
Schwefel(x1,x2,x3): MACRO real =
(x1-x2^2)^2+(x2-1)^2+(x1-x3^2)^2+(x3-1)^2
Schwefel_forall_: LEMMA
-10<=x1 AND x1<=10 AND -10<=x2 AND x2<=10 AND -10<=x3 AND x3<=10 IMPLIES
Schwefel(x1,x2,x3) >= -0.00000000058806
Schwefel_exists_: LEMMA
EXISTS (x1,x2,x3):
-10<=x1 AND x1<=10 AND -10<=x2 AND x2<=10 AND -10<=x3 AND x3<=10 AND
Schwefel(x1,x2,x3) <= 0.00000000058806
ReactionDiffusion(x1,x2,x3): MACRO real =
-x1+2*x2-x3-0.835634534*x2*(1+x2)
ReactionDiffusion_forall_: LEMMA
-5<=x1 AND x1<=5 AND -5<=x2 AND x2<=5 AND -5<=x3 AND x3<=5 IMPLIES
ReactionDiffusion(x1,x2,x3) >= -36.7126907 % Paper answer is -10.4057
ReactionDiffusion_exists_: LEMMA
EXISTS (x1,x2,x3):
-5<=x1 AND x1<=5 AND -5<=x2 AND x2<=5 AND -5<=x3 AND x3<=5 AND
ReactionDiffusion(x1,x2,x3) <= -36.7126
Chebyshev1 : LEMMA
abs(x) <= 1 IMPLIES (2*x^2 -1)^2 <= 1
Chebyshev2 : LEMMA
abs(x) <= 1 IMPLIES (4*x^3 -3*x)^2 <= 1
END benchmarks
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
