|
%% examples4Q.pvs
%%
%% These examples only deal with rational expressions, for that reason the theory
%% just imports strategies4Q.
%%
examples4Q : theory
BEGIN
IMPORTING strategies4Q
x,y : var real
%%%% Examples of numerical
zero_to_one_quarter : LEMMA
x ## [|0,1|] IMPLIES
x*(1-x) ## [|0.0000, 0.2501|]
%% The expression (! 1 1) refers to formula 1, 1st term, i.e., x*(1-x)
%|- zero_to_one_quarter : PROOF
%|- (then (skeep) (numerical (! 1 1) :precision 4 :maxdepth 20 :verbose? t))
%|- QED
x0,x1,x2,x3,x4,x5,x6,x7 : VAR real
Heart(x0,x1,x2,x3,x4,x5,x6,x7): MACRO real =
-x0*x5^3+3*x0*x5*x6^2-x2*x6^3+3*x2*x6*x5^2-x1*x4^3+3*x1*x4*x7^2-x3*x7^3+3*x3*x7*x4^2-0.9563453
hdp_mm: LEMMA
-0.1 <= x0 AND x0 <= 0.4 AND
0.4 <= x1 AND x1 <= 1 AND
-0.7 <= x2 AND x2 <= -0.4 AND
-0.7 <= x3 AND x3 <= 0.4 AND
0.1 <= x4 AND x4 <= 0.2 AND
-0.1 <= x5 AND x5 <= 0.2 AND
-0.3 <= x6 AND x6 <= 1.1 AND
-1.1 <= x7 AND x7 <= -0.3 IMPLIES
Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [|-1.852, 1.518|]
%% The expression (! 1 1) refers to formula 1, 1st term, i.e., polynomial Heart
%|- hdp_mm : PROOF
%|- (then (skeep) (numerical (! 1 1) :verbose? t))
%|- QED
%%%% Examples of interval
hdp_minmax: LEMMA
-0.1 <= x0 AND x0 <= 0.4 AND
0.4 <= x1 AND x1 <= 1 AND
-0.7 <= x2 AND x2 <= -0.4 AND
-0.7 <= x3 AND x3 <= 0.4 AND
0.1 <= x4 AND x4 <= 0.2 AND
-0.1 <= x5 AND x5 <= 0.2 AND
-0.3 <= x6 AND x6 <= 1.1 AND
-1.1 <= x7 AND x7 <= -0.3 IMPLIES
Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [| -1.76, 1.46 |]
%|- hdp_minmax : PROOF
%|- (then (skeep) (interval))
%|- QED
common_point: LEMMA
EXISTS (x,y,z:real): abs(x) <= 10 AND abs(y) <= 10 AND z ## [|0,1/2|] AND
LET x2 = x^2,
y2 = y^2 IN
x2-2*x+1+y2-2*y+1<1 AND x2 + y2 < 3-2*y+0.01
%|- common_point : PROOF (interval :verbose? t) QED
Eps : posreal = 0.0001
simple_ite : LEMMA
FORALL (x:real | x ## [| 0, 10 |]) :
IF x <= 1 THEN sq(x) <= x+Eps
ELSE sq(x) >= x-Eps
ENDIF
%|- simple_ite : PROOF
%|- (interval)
%|- QED
END examples4Q
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
