topics KNOPPIX/Math DVD maxima KSEG GeoGebra Coq 2011 July 17 - Page 1

Size: px

Start display at page:

Download "topics KNOPPIX/Math DVD maxima KSEG GeoGebra Coq 2011 July 17 - Page 1"

あきみみつだ
7 years ago
Views:

1 KNOPPIX/Math ( ) 2011/07/17

2 topics KNOPPIX/Math DVD maxima KSEG GeoGebra Coq 2011 July 17 - Page 1

3 (1) 2011 July 17 - Page 2

4 (2) 2011 July 17 - Page 3

5 KNOPPIX/Math KNOPPIX: Linux CD/DVD CD/DVD 1 Windows PC Mac KNOPPIX/Math x Math KnxmLauncher KNOPPIX-Math-Start WEB DVD KNOPPIX/Math Project ( July 17 - Page 4

6 maxima Macsyma MIT( ) Project MAC ( 60s 80s...) DOE Macsyma maxima MIT Slagle ( 60 ) (heuristics) 90% Risch Moses (MIT) Reduce, Risa/Asir( / ), Axiom Maple, Mathematica( ) 2011 July 17 - Page 5

7 (wx)maxima wxmaxima Shift-Enter ( Calulus) (Integrate) x y x*y x y x^y e %e %pi %in %on n % (1) %e^(%e^(%e^(%e^(%e^(%e^x))))) (1.1) x OK differentiate(%, x) (1.2) x OK integrate(%, x) 2011 July 17 - Page 6

8 (2) log(x)dx. 1 (3) x 3 1 dx 1 dx x 4 1 (3.1) (3.2) (simplify) (Simplify) Macsyma (4) factor(x^4-1), factor(x^8-1), factor(x^20-1), factor(x^20-2*x^10+1) (Factor) (5) nusum(k^2,k,1,n) n k=1 k 2 k 2, k, 1 n 2011 July 17 - Page 7

9 KSEG DVD KSEG KSEG shift July 17 - Page 8

10 KSEG (1) (a) (a.1) (a.2) (a.3) Shift (a.4) (a.5) (b) (b.1) (b.2) (b.3) Shift (b.4) (b.5) 2011 July 17 - Page 9

11 KSEG (2) (c) (c.1-3) (c.4) (c.5) (d) (e) 3 2 (f) / / (g) (h) 2011 July 17 - Page 10

12 KSEG (3) l l F (i.1) X-Y X X F F X Y (*) F (i.2) O X Y (i.3) F O F F, O O F (i.4) X F l F Y (i.5) P l P P l (i.6) F P F P F P (i.7) F, P P l P l (i.8) P P (i.9) F 2011 July 17 - Page 11

13 KSEG (4) (j.1) O 1, O 2 (j.2) O 1 O 2 AB (j.3) AB P (j.4) AP BP (j.4) AP O 1 AP (j.5) O 2 P B (*) P (j.6) (j.7) P AB AB P AB 2011 July 17 - Page 12

14 GeoGebra (1) 5 [ ] 3 (2) 4 [ ] (3) 2 [2 ] 2 (4) 4 [ ] (5) [2 ] (6) 6 [ 1 ] (*)? 3 Surf 2011 July 17 - Page 13

15 2011 July 17 - Page 14

16 ? 2011 July 17 - Page 15

17 ? 2011 July 17 - Page 16

18 Coq logic or = 0 ; n (Suc n) Suc successor Isabelle, HOL, Coq... Coq 2 n k=0 k = n(n + 1) n k sum n Suc p S p k= July 17 - Page 17

19 Fixpoint sum (n:nat) {struct n} : nat := (* {struct...} n *) match n with 0 => 0 (* n 0 0 *) (S p) => (S p) + (sum p) (* n (S p) p+1 (p+1)+(sum p) *) end. Theorem sumof 1ton: forall x:nat, 2*(sum x) = x*(x+1) sumof 1ton induction induction x. x=0 2*(sum 0) = 0*(0 + 1) auto. OK. (S x) 2*(sum x) = x * (x + 1) IHx 2*(sum (S x)) = (S x) * ((S x) + 1) Lemma sub: forall n:nat, sum (S n) = (S n) + (sum n). (Theorem ) auto. Qed. rewrite sub. (* sub *) (* 2*((S x) + (sum x) *) Require Import Arith. (* *) rewrite mult plus distr l. (* *) (* 2*(S x) + 2*(sum x) *) rewrite IHx. (* IHx *) (* 2*(S x) + x*(x + 1) *) Require Import ArithRing. ring. (* *) Qed July 17 - Page 18

(S x) 2*(sum x) = x * (x + 1) IHx 2*(sum (S x)) = (S x) * ((S x) + 1) Lemma sub: forall n:nat, sum (S n) = (S n) + (sum n). (Theorem ) auto. Qed. rewrite sub.

20 ... JSEC(Japan Science & Engineering Challenge) 2008 Mathematica Rubik GAP fujimoto/rubik.html Gröbner backtrack (?) 2011 July 17 - Page 19

種々の数学ソフトウェア

種々の数学ソフトウェア January 17, 2013 Maple, Maxima, GeoGebra,,, Knoppix/Math Maple,, : Student[Calculus1] : 30 ( 2 ) Maple Doc Maple ( ) cfep, ; ab a*b, x n xˆn x n + x m, xˆn, x n+xm Maple ( ) =, =!= f(x):=xˆ3-3*x+1;