Quelle  tarski_examples.pvs   Sprache: PVS

tarski_examples: THEORY
BEGIN

  IMPORTING Tarski@strategies

  example_fall : LEMMA
    FORALL (x:real): x^3 < 0 OR x*x*x > 0 OR x^2 = 0
%|- example_fall : PROOF
%|- (tarski)
%|- QED

  example_ex : LEMMA
    EXISTS (x:real) : x^3 = x AND x^2 = x
%|- example_ex : PROOF
%|- (tarski)
%|- QED

  example_1: LEMMA
    FORALL(y,x,z:real): (x-2)^2*(-x+4)>0 AND x^2*(x-3)^2>=0 AND x-1>=0 AND -(x-3)^2+1>0
    IMPLIES
    -(x-11/12)^3*(x-41/10)^3>=0 
%|- example_1 : PROOF
%|- (tarski)
%|- QED

  example_2: LEMMA
    FORALL (x:real): x>=-9 AND x<10 AND x^4>0 IMPLIES x^12>0
%|- example_2 : PROOF
%|- (tarski)
%|- QED

  example_3: LEMMA
    EXISTS (x:real): 
      (x-2)^2*(-x+4)>0 AND x^2*(x-3)^2>=0 AND x-1>=0 AND -(x-3)^2+1>0 AND
     -(x-11/12)^3*(x-41/10)^3<1/10
%|- example_3 : PROOF
%|- (tarski)
%|- QED

  example_4 : LEMMA
    EXISTS (x:real):
      x^5 - x - 1 = 0
      AND 
      x^12 + 425/23*x^11 - 228/23*x^10 - 2*x^8 
      - 896/23*x^7 - 394/23*x^6 + 456/23*x^5 + x^4 
      + 471/23*x^3 + 645/23*x^2 - 31/23*x - 228/23= 0 
      AND x^3 + 22*x^2 -31 >=0 
      AND x^22 -234/567*x^20 -419*x^10+ 1948>0
%|- example_4 : PROOF
%|- (tarski)
%|- QED

 example_5 : LEMMA
   FORALL (x:real): x^2 >= 1 IMPLIES abs(x) >= 1
%|- example_5 : PROOF
%|- (tarski)
%|- QED

END tarski_examples