Stufen

Anforderungen | Konzepte | Entwurf | Entwicklung | Qualitätssicherung | Lebenszyklus | Steuerung

Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Imperative_HOL/ex/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 25 kB

Quelle examples.pvs Sprache: PVS

examples: THEORY
BEGIN

  IMPORTING 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 examples

quality95%

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

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.

Neuigkeiten

Aktuelles

Motto des Tages

Software

Produkte

Quellcodebibliothek

Aktivitäten

Artikel über Sicherheit

Anleitung zur Aktivierung von SSL

Muße

Gedichte

Musik

Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge

Impressum | Ethik und Gesetz | Haftungsausschluß | Kontakt | Seitenstruktur | ^© 2026 JDD |

Seite erzeugt: Seite erzeugt: 2026-04-01 16:05:26