| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Tarski/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle examples.pvs Sprache: PVS |
|||||||||
|
examples: THEORY
BEGIN IMPORTING 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 examples ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28