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

quality98%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.