|
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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
