| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/examples/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle interval_examples4Q.pvs Sprache: PVS |
|||||||||
|
%% interval_examples4Q.pvs
%% %% These examples only deal with rational expressions, for that reason the theory %% just imports strategies4Q. %% interval_examples4Q : theory BEGIN IMPORTING interval_arith@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* 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 interval_examples4Q ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28