
products/Sources/formale Sprachen/PVS/examples/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sturm_examples.pvs Sprache: PVS

Original von: PVS^©

sturm_examples: THEORY
BEGIN

  IMPORTING Sturm@strategies

  x : VAR real

  example_1: LEMMA
    160*((x-1/2)^2*(x-9)^4*(x+8.5)^2 + 0.1) /= 0
%|- example_1 : PROOF
%|- (sturm)
%|- QED

  example_2: LEMMA FORALL (x:real):
     (x-1/2)^2*(x-9)^4*(x+8.5)^2 >= 0
%|- example_2 : PROOF
%|- (sturm)
%|- QED

example_3: LEMMA
  (x^16-x^15-3*x^13+x^12-x^11+2*x^10-6*x^9+8*x^8
   -7*x^7-6*x^6+5*x^5+4*x^4-3*x^3+350*x + 478)^2 /= 0
%|- example_3 : PROOF
%|- (sturm)
%|- QED

  example_4: LEMMA
    x<0 IMPLIES x^101 < -x
%|- example_4 : PROOF
%|- (sturm)
%|- QED

  example_5: LEMMA
    x<0 IMPLIES x^5-2*x^3 < 6
%|- example_5 : PROOF
%|- (sturm)
%|- QED

  example_6: LEMMA x^2 - 2*x + 1 >= 0
%|- example_6 : PROOF
%|- (sturm)
%|- QED

  example_7: LEMMA x*(1-x) <= 1/4
%|- example_7 : PROOF
%|- (sturm)
%|- QED

%% Examples with quantifications in antecedent and consequent

example_8: LEMMA
   EXISTS (x:real) : x >= 0 AND x^2 - x < 0
%|- example_8 : PROOF
%|- (sturm)
%|- QED

example_n8: LEMMA
   NOT (FORALL (x:real) : x >= 0 IMPLIES x^2 >= x)
%|- example_n8 : PROOF
%|- (sturm -1)
%|- QED

example_80: LEMMA
   EXISTS (x:real) : x >= 0 AND x^2 - x = 0
%|- example_80 : PROOF
%|- (sturm)
%|- QED

example_n80: LEMMA
   NOT (FORALL (x:real) : x >= 0 IMPLIES x^2 /= x)
%|- example_n80 : PROOF
%|- (sturm -1)
%|- QED

example_9: LEMMA
   FORALL (x:real) : x<0 IMPLIES x^5 < -x
%|- example_9 : PROOF
%|- (sturm)
%|- QED

example_n9: LEMMA
   NOT (EXISTS (x:real): x < 0 AND x^5 >= -x)
%|- example_n9 : PROOF
%|- (sturm -1)
%|- QED

example_90: LEMMA x<0 IMPLIES x^5 /= 0
%|- example_90 : PROOF
%|- (sturm)
%|- QED

example_n90: LEMMA
   NOT (EXISTS (x:real): x < 0 AND x^5 = 0)
%|- example_n90 : PROOF
%|- (sturm -1)
%|- QED

  example_10 : LEMMA
    NOT EXISTS (x:posreal) : x^3 <= 0
%|- example_10 : PROOF
%|- (sturm -1)
%|- QED

  example_11 : LEMMA
    FORALL (x:real | abs(x) <= 1) : (x-1)*(x+1) <= 0
%|- example_11 : PROOF
%|- (sturm)
%|- QED

  example_12: LEMMA
    x^120-2*x^60+1 >= 0
%|- example_12 : PROOF
%|- (sturm)
%|- QED

  legendre : LEMMA
    abs(x) < 1 IMPLIES
    3969/65536 + 63063/4096 * x^6 + 1792791/4096 * x^10 +
    3002285/4096 * x^18 + 6600165/4096 * x^14
    - 72765/65536 * x^4 - 3558555/32768 * x^8
    - 10207769/65536 * x^20 - 35043645/32768 * x^12
    - 95851899/65536 * x^16 > 0
%|- legendre : PROOF
%|- (sturm)
%|- QED

  legendre3 : LEMMA
    abs(x) < 1 IMPLIES
    (3969/65536 + 63063/4096 * x^6 + 1792791/4096 * x^10 +
     3002285/4096 * x^18 + 6600165/4096 * x^14
     - 72765/65536 * x^4 - 3558555/32768 * x^8
     - 10207769/65536 * x^20 - 35043645/32768 * x^12
     - 95851899/65536 * x^16)^3 > 0
%|- legendre3 : PROOF
%|- (sturm)
%|- QED

  harrison_sos : LEMMA
    ((x-1)^8 + 2*(x-x)^8 + (x-3)^8 -2)/4 >= 0
%|- harrison_sos : PROOF
%|- (sturm)
%|- QED

%% Examples with interval notations, including extended intervals, i.e.,
%% reals@RealInt and interval_arith@interval

  example_13 : LEMMA
    FORALL (x:real | x ## [|-2,1|]) : x^4-x^3-19*x^2-11*x+30 <= 31.7
%|- example_13 : PROOF
%|- (sturm)
%|- QED

  example_14 : LEMMA
    FORALL (x:real) : x ## [| 0, oo |] IMPLIES -x^3 <= 0
%|- example_14 : PROOF
%|- (sturm)
%|- QED

  example_15 : LEMMA
    FORALL (x:real) : x ## [| open(1), oo |] IMPLIES -x^3 < 1
%|- example_15 : PROOF
%|- (sturm)
%|- QED

  example_16 : LEMMA
    FORALL (x:real) : x ## [| -oo, 1 |] IMPLIES x*(1-x) <= 0.25
%|- example_16 : PROOF
%|- (sturm)
%|- QED

  example_17 : LEMMA
    FORALL (x:real): x>0 IMPLIES x^15*(2-x)^20*(6-x)^2*(12-x)^4*(20-x)^6>=0
%|- example_17 : PROOF
%|- (sturm)
%|- QED

% Examples of monotonicity

  mono_example_1 : LEMMA
    FORALL (x,y:real) : x >= 1 AND x < y IMPLIES (x-1/4)^2 <= y*y-(1/2)*y+(1/16)
%|- mono_example_1 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_2 : LEMMA
    FORALL (x,y:real) : x < y IMPLIES x^5 /= y^5
%|- mono_example_2 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_3: LEMMA
    FORALL (x,y:real) : 0.4 <= x AND x < y AND y <= 0.6 IMPLIES
    x^5-x^3+x/5>y*(y^4-y^2+1/5)
%|- mono_example_3 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_4: LEMMA
    FORALL (x,y:real): x /= y IMPLIES x^3 /= y^3
%|- mono_example_4 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_5: LEMMA
    EXISTS (x,y:real): x < y AND x^2 >= sq(y)
%|- mono_example_5 : PROOF
%|- (mono-poly)
%|- QED

  mono_example_6: LEMMA
    EXISTS (x:real,y:real|y>=-1): x > y AND x^4 < y^4
%|- mono_example_6 : PROOF
%|- (mono-poly)
%|- QED

END sturm_examples

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Bot Zugriff