Täs­tä voit ko­pioi­da han­ka­las­ti näp­päil­tä­viä merk­ke­jä:
¬ Γ Δ Θ Λ Ξ Π Σ Φ Ψ Ω α β γ δ ε ζ η θ ι κ λ μ ν ξ π ρ σ τ υ φ χ ψ ω ϑ ϕ ϵ ← → ↔ ↠ ⇐ ⇒ ⇔ ∀ ∃ − √ ∧ ∨ ≠ ≡ ≤ ≥ ⋅ ⌈ ⌉ ⌊ ⌋ 𝗙 𝗧 𝗨

Ylei­nen Math­Check-apu­si­vu

Pit­kä Math­Check-oh­je (uu­teen vä­li­leh­teen)

Täl­lä si­vul­la voit tar­kas­taa las­kel­mia­si ja päät­te­lyi­tä­si sii­nä mää­rin kuin Math­Check pys­tyy nii­tä tar­kas­ta­maan. Mo­nes­ta Math­Checkin ym­mär­tä­mäs­tä teh­tä­vä­la­jis­ta on syö­tet­ty val­miik­si yk­si tai kak­si esi­merk­kiä. Ko­kei­le nii­tä ja/tai pyy­hi ne pois ja kir­joi­ta oma las­kel­ma­si tai päät­te­ly­si ti­lal­le. Vas­taus­ruu­dun ko­koa voi sää­tää sen oi­keas­ta ala­kul­mas­ta.

Arit­meet­ti­sen lau­sek­keen sie­ven­tä­mi­nen
(Epä)yh­tä­lö(ryh­män) rat­kai­se­mi­nen
Pro­po­si­tio­lo­gii­kan lau­sek­keen sie­ven­tä­mi­nen
Li­neaa­ri­nen luon­nol­lis­ten, ko­ko­nais- tai reaa­li­lu­ku­jen pre­di­kaat­ti­lo­giik­ka
Tau­luk­ko­väit­tä­mien ver­taa­mi­nen
Lau­se­ke­puun piir­tä­mi­nen
Lau­se­ke­pui­den ver­taa­mi­nen
Merk­ki­jo­non jä­sen­nys­puu
Kie­li­op­pien ver­taa­mi­nen
Funk­tion ku­vaa­ja
Muu­ta

Arit­meet­ti­sen lau­sek­keen sie­ven­tä­mi­nen

Math­Check tar­kas­taa sie­ven­nök­siä tes­taa­mal­la useil­la muut­tu­jien ar­vo­yh­dis­tel­mil­lä. Tar­kas­tus­ta­pa ei ole täy­del­li­nen, mut­ta huo­maa mel­ko var­mas­ti muut vir­heet kuin eroa­vai­suu­det ni­mit­tä­jien nol­la­koh­dis­sa. Jos ha­luat tar­kas­taa usei­ta sie­ven­nök­siä sa­mal­la ker­taa, kir­joi­ta nii­den vä­liin arithmetic. Muut­tu­jat i, …, n ja I, …, N ovat ole­tus­ar­voi­ses­ti ko­ko­nais­lu­ku­ja ja muut reaa­li­lu­ku­ja, mut­ta muut­tu­jan tyy­pin voi myös aset­taa. Tar­kas­tuk­ses­sa käy­tet­tä­vää muut­tu­jien ar­vo­aluet­ta voi ra­joit­taa assume-ra­ken­teel­la (jon­ka lo­pus­sa on puo­li­pis­te). Jos ra­joi­tat ar­vo­aluet­ta ko­vin voi­mak­kaas­ti, vir­hei­den huo­maa­mis­ky­ky heik­ke­nee.

ok_text Oi­kein! arithmetic (a+b)^2 = a^2 + 2a b + b^2 = a^2 + 2a b + b^2 + (a-b)^2 - (a-b)^2 = a^2 + 2a b + b^2 + (a^2 - 2a b + b^2) - (a-b)^2 = 2a^2 + 2b^2 - (a-b)^2 /* Kos­ka `(a-b)^2 >= 0` */ <= 2a^2 + 2b^2 = DD b 2b(a^2 + b^2/3) arithmetic real n/*Ko­kei­le myös pois­taa tä­mä ri­vi!*/ assume n >= 0 /\ x >= -1; (1+x)^(n+1) = (1+x)(1+x)^n >= (1+x)(1+n x) = 1 + n x + x + n*x^2 >= 1 + n x + x = 1 + (n+1)x tai

(Epä)yh­tä­lö(ryh­män) rat­kai­se­mi­nen

Täs­sä toi­min­ta­moo­dis­sa Math­Check te­kee pe­riaat­tees­sa täy­del­lis­tä työ­tä (olet­taen, et­tä kaik­ki tar­vit­ta­vat las­kel­mat mah­tu­vat tie­to­ko­neen lu­ku­aluee­seen, ja et­tä oh­jel­moin­ti­vir­hei­tä ei ole). Hin­ta­na on, et­tä muut­tu­jien ker­to­las­ku­ja (ja sik­si myös­kään esi­mer­kik­si muut­tu­jien ne­liöi­tä) ei voi­da kä­si­tel­lä, lo­ga­rit­meis­ta yms. pu­hu­mat­ta­kaan. Ja­ko­las­ku sal­li­taan, jos sii­tä ei sie­ven­net­täes­sä syn­ny muut­tu­jien ker­to­las­ku­ja. Myös kvant­to­rien käyt­tö on sal­lit­tua. Ko­vin mo­ni­mut­kai­set väit­tä­mät voi­vat saa­da Math­Checkin tu­keh­tu­maan. Kaik­ki muut­tu­jat ovat reaa­li­lu­ku­ja.

ok_text Oi­kein! real_logic solve_all f_simplify |x+2| = 3x + 18 <=> x+2 < 0 /\ -(x+2) = 3x + 18 \/ x+2 >= 0 /\ x+2 = 3x + 18 subproof assume x+2 < 0; -(x+2) = 3x + 18 <=> 0 = x+2+3x+18 <=> 4x = -20 <=> x = -5 subend subproof assume x+2 >= 0; x+2 = 3x + 18 <=> 0 = -x-2+3x+18 <=> 2x = -16 <=> x = -8 <=> FF /*, kos­ka `-8+2 >= 0` ei pä­de*/ subend original <=> x = -5 \/ FF <=> x = -5 tai

Pro­po­si­tio­lo­gii­kan lau­sek­keen sie­ven­tä­mi­nen

Täs­sä toi­min­ta­moo­dis­sa Math­Check te­kee täy­del­lis­tä työ­tä — pois­lu­kien mah­dol­li­set oh­jel­moin­ti­vir­heet. Math­Check käyt­tää ai­na­kin kah­ta to­tuus­ar­voa F ja T. Voit va­li­ta, on­ko myös kol­mas to­tuus­ar­vo U eli ”mää­rit­te­le­mä­tön” käy­tös­sä. Käy­tet­tä­vis­sä ovat pro­po­si­tio­lo­gii­kan ope­raat­to­rit ¬ ∧ ∨ → ↔ && || ↠, päät­te­ly­ope­raat­to­rit ⇐ ⇒ ⇔ ≡ se­kä ali­päät­te­lyt. Ope­raat­to­ri ⇔ sa­mais­taa ja ≡ ei sa­mais­ta to­tuus­ar­vot U ja F. Ope­raat­to­rit && ja || koh­te­le­vat mää­rit­te­le­mä­tön­tä ku­ten oh­jel­moin­ti­kie­lis­sä, ja ↠ on Łu­ka­sie­wic­zin imp­li­kaa­tio.

ei ole on
ok_text Oi­kein! !P /\ !Q \/ P /\ !Q \/ P /\ Q subproof #(P /\ !Q \/ P /\ Q#) <=> P /\ (!Q \/ Q) <=> P /\ TT <=> P /*Kos­ka `P <=> P \/ P /\ X`*/ <=> P \/ P /\ !Q subend original <=> #(!P /\ !Q#) \/ #(P \/ P /\ !Q#) <=> P \/ !P /\ !Q \/ P /\ !Q <=> P \/ (!P \/ P) /\ !Q <=> P \/ TT /\ !Q <=> P \/ !Q <=> Q --> P tai

Li­neaa­ri­nen luon­nol­lis­ten, ko­ko­nais- tai reaa­li­lu­ku­jen pre­di­kaat­ti­lo­giik­ka

Näis­sä­kin toi­min­ta­moo­deis­sa Math­Check te­kee täy­del­lis­tä työ­tä — edel­lä mai­ni­tuil­la va­rauk­sil­la. Edel­lä mai­ni­tun pro­po­si­tio­lo­gii­kan ka­lus­ton (pait­si ↠) li­säk­si käy­tet­tä­vis­sä ovat ver­tai­lu­ope­raat­to­rit = ≠ < ≤ ≥ > ja kvant­to­rit ∀ ∃. Nii­tä voi­daan so­vel­taa arit­meet­ti­siin ter­mei­hin. Ter­meis­sä voi ol­la va­kioi­ta, muut­tu­jia, yh­teen­las­ku­ja ja va­kioil­la ker­to­mi­sia. Luon­nol­lis­ten lu­ku­jen ta­pauk­ses­sa ter­meis­sä voi ol­la myös ope­raat­to­rei­ta mod ja div. Reaa­li­lu­ku­jen ta­pauk­ses­sa ne ei­vät ole sal­lit­tu­ja, mut­ta vä­hen­nys­las­ku ja it­seis­ar­vo se­kä jois­sa­kin ti­lan­teis­sa ja­ko­las­ku ovat.

Reaa­li­lu­ku­jen ta­paus on it­se asias­sa sa­ma toi­min­ta­moo­di kuin edel­lä mai­nit­tu (Epä)yh­tä­lö(ryh­män) rat­kai­se­mi­nen sil­lä ero­tuk­sel­la, et­tä siel­lä vaa­di­taan lop­pu­tu­lok­sen ole­van rat­kais­tu kaik­kien muut­tu­jien suh­teen, mut­ta täs­sä al­la ei vaa­di­ta.

Ko­ko­nais­lu­ku­jen toi­min­ta­moo­di on uu­sin ja mo­ni­puo­li­sin (mut­ta tä­tä kir­joi­tet­taes­sa puut­teel­li­ses­ti tes­tat­tu). Sii­nä ter­meis­sä voi ol­la va­kioi­ta, muut­tu­jia, yh­teen- ja vä­hen­nys­las­ku­ja, va­kioil­la ker­to­mi­sia, it­seis­ar­vo­ja, ope­raat­to­rei­ta mod ja div se­kä joi­ta­kin bi­tit­täi­siä loo­gi­sia ope­raat­to­rei­ta. Iso­ja kir­jai­mia voi­daan mää­ri­tel­lä tar­koit­ta­maan pro­po­si­tioi­ta tai pa­ra­met­roi­tu­ja kaa­vo­ja. Li­säk­si voi­daan pyy­tää tu­los­ta­maan ter­min tai kaa­van esi­tys de­ter­mi­nis­ti­se­nä ää­rel­li­se­nä au­to­maat­ti­na.

luon­nol­li­set lu­vut ℕ ko­ko­nais­lu­vut ℤ reaa­li­lu­vut ℝ
ok_text Oi­kein! EE y: y < x <=> ! EE z: x < z < x+1 presburger !(EE a: EE b: EE c: n = 6a + 9b + 20c) /\ AA m; m > n: EE a: EE b: EE c: m = 6a + 9b + 20c <=> n = 43 zburger define P(x) === x >= 0; define E(n) === ! EE x: P(x) /\ EE y: EE z: y >= 0 /\ P(z) /\ 6x + 9y + 20z = n; !( E(n) /\ !EE m: m > n /\ E(m) ) real_logic /*Tut­ki­taan erään pa­loit­tain mää­ri­tel­lyn fun­tion jat­ku­vuut­ta pis­tees­sä `(7,8/3)`.*/ assume ep > 0; EE de; de > 0: AA x: EE y: (x<7 /\ y=7/3 \/ x>=7 /\ y=8/3) /\ (|x-7| < de --> |y-8/3| < ep) tai

Tau­luk­ko­väit­tä­mien ver­taa­mi­nen

Tau­luk­ko­väit­tä­mien ver­taa­mi­nen on las­ken­nal­li­ses­ti hy­vin vai­keaa. Mi­kään oh­jel­ma ei voi sel­vi­tä sii­tä täy­del­li­ses­ti. Math­Check ver­taa väit­tä­mät ko­kei­le­mal­la muu­ta­mal­la pie­nel­lä tau­lu­kol­la, joi­den al­kiot ovat ko­ko­nais­lu­ku­ja vä­lil­tä 0, …, 3. Täl­lä ta­val­la saa­daan kiin­ni suu­ri osa väit­tä­mien erois­ta, mut­ta ei kaik­kia. Kan­nat­taa ver­ra­ta ope­raat­to­ril­la === ei­kä <=>, kos­ka jäl­kim­mäi­nen ei kat­so vir­heek­si ti­lan­tei­ta, jois­sa toi­nen tuot­taa F ja toi­nen on mää­rit­te­le­mä­tön.

ok_text Oi­kein! array_claim Il­moi­ta täs­sä tau­lu­kon ni­mi ja in­dek­si­alue: A[1...n]
AA i; 1 <= i < n: A[i] <= A[i+1] === AA i: AA j; 1 <= i < j <= n: A[i] <= A[j] === AA i: AA j; 1 <= i < j <= n: A[i] < A[j] tai

Lau­se­ke­puun piir­tä­mi­nen

Jos ha­luat mon­ta lau­se­ke­puu­ta, ero­ta lau­sek­keet puo­li­pis­teel­lä. Jos ha­luat et­tä muut­tu­ja tul­ki­taan pro­po­si­tiok­si, käy­tä isoa kir­jain­ta.

ok_text Oi­kein! expression_tree (a+b)^2 = (a+b)(a+b) = (a a + a b) + (b a + b b) = a^2 + 2a b + b^2 /*Jos ha­luat mon­ta lau­se­ke­puu­ta, ero­ta lau­sek­keet puo­li­pis­teel­lä.*/ ; !P \/ UU === P --> UU <=> FF --> TT tai

Lau­se­ke­pui­den ver­taa­mi­nen

Val­mii­na an­net­tu esi­merk­ki ha­vain­nol­lis­taa, et­tä nä­ky­mä­tön ker­to­las­ku ja * eli ⋅ ovat eri ope­raat­to­ri, vaik­ka niil­lä on­kin sa­ma mer­ki­tys. Esi­merk­ki ha­vain­nol­lis­taa myös, et­tä Math­Check jät­tää tur­hat su­lut huo­miot­ta.

ok_text Lau­sek­keet ovat syn­tak­ti­ses­ti sa­mat! tree_compare (a+b)^2 = a^2 + 2a b + b^2; (a+b)^2 = (a^2 + (2a b)) + (b^2); (a+b)^2 = a^2 + 2a*b + b^2 tai

Merk­ki­jo­non jä­sen­nys­puu

Kir­joi­ta ylem­pään ruu­tuun kie­li­op­pi BNF:llä esi­tet­ty­nä ja alem­paan ruu­tuun merk­ki­jo­no. Math­Check ker­too kuu­luu­ko merk­ki­jo­no kie­leen ja jos kuu­luu, niin piir­tää jä­sen­nys­puun. Täs­sä Math­Check te­kee täy­del­lis­tä työ­tä, kun­han tar­kas­tus­teh­tä­vä ei pai­su liian isok­si ja olet­taen et­tä oh­jel­moin­ti­vir­hei­tä ei ole.

ok_text Oi­kein! CFG_set S ::= T | S+T | S-T T ::= A | TA | T*A A ::= x | y | 1 | 2 | 3 | (S) ; CFG_tree 2+(x+y)(x-1) tai

Kie­li­op­pien ver­taa­mi­nen

Kir­joi­ta mo­lem­piin ruu­tui­hin kie­li­op­pi. Math­Check ver­taa, tuot­ta­vat­ko ne sa­man kie­len. Tä­mä on las­ken­nal­li­ses­ti mah­do­ton teh­tä­vä, jo­ten Math­Check voi sel­vi­tä sii­tä vain osit­tain. Math­Check ei huo­maa ero­ja, jot­ka il­me­ne­vät vain pit­kil­lä merk­ki­jo­noil­la.

Kiel­lä mo­ni­se­lit­tei­syys
ok_text Kie­let ovat luul­ta­vas­ti sa­mat! CFG_set S ::= T | S+T | S-T T ::= A | TA | T*A A ::= x | y | 1 | 2 | 3 | (S) ; CFG_set2 S ::= A | S+S | S-S | S*S | SS A ::= (S) | 1 | 2 | 3 | x | y ; CFG_compare tai

Funk­tion ku­vaa­ja

Mo­net muut oh­jel­mat piir­tä­vät käy­riä Math­Checkia pa­rem­min, mut­ta jos Math­Checkin piir­tä­mä ku­va riit­tää, niin sel­viät vä­hem­mäl­lä oh­jel­mas­ta toi­seen vaih­te­le­mi­sel­la. Ylem­mäs­sä ruu­dus­sa ole­vis­ta ku­va-aluet­ta oh­jaa­vis­ta lu­vuis­ta voi jät­tää osan tai kaik­ki pois, jol­loin Math­Check va­lit­see niil­le ar­vot it­se. Tie­ten­kin voit myös muut­taa lu­ku­ja.

ok_text Oi­kein! draw_function -5 20 -18 100 ; (a+1)^2; (a+1)/(a-1); 50 log (a+1) tai

Muu­ta

Math­Checkis­sa on myös yh­tä­lö­moo­di, jo­ka sal­lii ne­liöt, kor­keam­man as­teen po­ly­no­mit, po­tens­sit, tri­go­no­met­ri­set funk­tiot ja lo­ga­rit­mit, mut­ta jol­la on kak­si mer­kit­tä­vää ja yk­si kes­kin­ker­tai­nen hait­ta edel­lä mai­nit­tuun näh­den: muut­tu­jia voi ol­la vain yk­si, opet­ta­jan on syö­tet­tä­vä juu­ret, ja pa­lau­te vir­heen vuok­si syn­ty­nees­tä yli­mää­räi­ses­tä juu­res­ta voi tul­la opis­ke­li­jal­le vii­veel­lä. Sii­hen voi tu­tus­tua tääl­lä. Haa­vee­na on jos­kus tu­le­vai­suu­des­sa laa­jen­taa edel­lä mai­nit­tua yh­tä­lö­moo­dia si­ten, et­tä yh­teen muut­tu­jaan saa so­vel­taa lo­ga­rit­me­ja yms., jol­loin tä­mä moo­di käy tar­peet­to­mak­si.

Math­Checkis­sa on myös mo­du­laa­ri­sen arit­me­tii­kan moo­di, jo­ka sal­lii täy­den pre­di­kaat­ti­lo­gii­kan päät­te­lyn jään­nös­luok­ka­ren­kaas­sa mo­du­lo M, mis­sä M on ko­ko­nais­lu­ku­va­kio ja 2 ≤ M ≤ 25. Sil­le ei ole täs­sä omaa esit­te­ly­ik­ku­naa, kos­ka sil­le on ol­lut vai­kea kek­siä ope­tus­käy­tön kan­nal­ta jär­ke­viä esi­merk­ke­jä.

Math­Checkis­sa on mo­nia ko­men­to­ja, joil­la opet­ta­ja voi vaa­tia, et­tä vas­taus on tiet­tyä muo­toa (esi­mer­kik­si tu­lo­jen sum­ma), tar­peek­si yk­sin­ker­tai­nen, rat­kais­tu tie­tyn muut­tu­jan suh­teen tai niin edel­leen.