| products/sources/formale Sprachen/PVS/while/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 92 kB |
|
Quelle field_examples.pvs Sprache: PVS |
|||||||||
|
%% Examples of strategies in Field 6.0
%% Cesar Munoz %% http://shemesh.larc.nasa.gov/people/cam/Field %% NASA LaRC field_examples : THEORY BEGIN a,b,c : VAR real pa,pb,pc : VAR posreal nza,nzb : VAR nzreal f1 : LEMMA a > 1 AND b > 1 => (a+1)/((a+1)/(b+1)) - b = 1 %|- f1 : PROOF (then (skeep) (field)) QED f2 : LEMMA b >1 AND a > 1 => (b-1)/((b-1)/(a-1)) - a = -1 %|- f2 : PROOF (then (skeep) (field)) QED f3 : LEMMA b >1 AND a > 1 => (b-1)/((b-1)/(a-1)) - a < 0 %|- f3 : PROOF (then (skeep) (field)) QED f4 : LEMMA (pa+1)/((pa+1)/(pb+1)) - pb >= 1 %|- f4 : PROOF (then (skeep) (field)) QED f5 : LEMMA (1+pb+(pa*pb+pa))/(1+pa) - pb = 1 %|- f5 : PROOF (then (skeep) (field)) QED f6 : LEMMA a > 1 IMPLIES a/((a-1) * (a+1)) - 1 /((a-1)*(a+1)) >= 1 /(a+1) - 1 %|- f6 : PROOF (then (skeep) (field)) QED f7: LEMMA 1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES 1/(1+ pb/(1+ 1/(1+pb))) = pa %|- f7 : PROOF (then (skeep) (field)) QED f8: LEMMA 1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES 1/(1+ pb/(1+ 1/(1+pb))) >= pa %|- f8 : PROOF (then (skeep) (field)) QED f9: LEMMA 1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES 1/(1+ pb/(1+ 1/(1+pb))) <= pa %|- f9 : PROOF (then (skeep) (field)) QED f10 : LEMMA a*(pa+b)/(pa+1) - b*(pa+a)/(pa+1) = 0 IMPLIES a = b %|- f10 : PROOF (then (skeep) (field - :cancel? t)) QED f11 : LEMMA a /= 1 IMPLIES 1 / (1-a) = 1 + a + a * a + (a*a*a)/(1-a) %|- f11 : PROOF (then (skeep) (field 2)) QED cf1 : LEMMA 4*(pa*pb) + (pa*6)*pa = pa*((c+1)*2) => 2*pb + 3*pa - 1 = c %|- cf1 : PROOF (then (skeep) (cancel-formula -)) QED cf2 : LEMMA 4*(pa*pb) + (pa*6)*pa <= pa*((c+1)*2) => 2*pb + 3*pa - c <= 1 %|- cf2 : PROOF (then (skeep) (cancel-formula -)) QED cf3 : LEMMA 4*((pa+1)*pb) + ((pa+1)*6)*(pa+1) = -(pa+1)*((c+1)*2) IMPLIES 2*pb + 3*(pa+1) + c + 1 = 0 %|- cf3 : PROOF (then (skeep) (cancel-formula -)) QED cf4 : LEMMA c+2 < 0 IMPLIES c*(c+2)*pa + pa*2*(c+2) > pb*pa*(c+2) %|- cf4 : PROOF (then (skeep) (cancel-formula)) QED cf5 : LEMMA c+2 < 0 AND c*(c+2)*pa + pa*2*(c+2) < b*pa*(c+2) IMPLIES b < 0 %|- cf5 : PROOF (then (skeep) (cancel-formula -2)) QED gr1 : LEMMA a /= -4 IMPLIES (a+3)*(a*a+9*a+20)/(a+4) = (a+3)*(a+5) %|- gr1 : PROOF (grind-reals) QED gr2 : LEMMA a /= 6 AND a /= 0 AND b = 3/(a*a-6*a) IMPLIES (a+3)/(a*(a-6)) = 1/(a-6)+b %|- gr2 : PROOF (grind-reals) QED gr3 : LEMMA a /= 6 AND a /=0 IMPLIES (a+3)/(a*(a-6)) = 1/(a-6)+3/(a*(a-6)) %|- gr3 : PROOF (grind-reals) QED %%% The following examples are taken from developments at NASA LaRC IMPORTING reals@sqrt A : VAR nzreal B,C,Delta,x : VAR real eps : VAR {x:real|x=1 OR x=-1} quadratic : LEMMA Delta = (B * B) - (4 * (A * C)) AND Delta >= 0 AND x = (eps * sqrt(Delta) - B) / (2 * A) IMPLIES A * x * x + B * x + C = 0 %|- quadratic : PROOF %|- (then (skeep :preds? t) (replaces (-6 -8)) (field 2)) %|- QED t,vix,viy,vox,voy,s : VAR real D : VAR posreal kb3d : LEMMA vox > 0 AND s*s - D*D > D AND s * vix * voy - s * viy * vox /= 0 AND ((s * s - D * D) * voy - D * vox * sqrt(s * s - D * D)) / (s * (vix * voy - vox * viy)) * s * vox /= 0 AND voy * sqrt(s * s - D * D) - D * vox /= 0 IMPLIES (viy * sqrt(s * s - D * D) - vix * D) / (voy * sqrt(s * s - D * D) - vox * D) = (D * D - s * s) / (((s * s - D * D) * voy - D * vox * sqrt(s * s - D * D)) / (s * (vix * voy - vox * viy)) * s * vox) + vix / vox %|- kb3d : PROOF (grind-reals) QED END field_examples ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28