Avaa oh­je:
arit­me­tiik­ka
sym­bo­likir­joi­ta
++
-
3y3y
y ⋅ 3y*3
(3 + 4)(x + 5)(3+4)(x+5)
x + 1
y + 6
 (x+1)/(y+6) 
2
3
4
2 3/4
|x + 1||x+1|
x2nx^(2n)
x + 1sqrt x+1
nx + 1root(n)(x+1)

Osa ei toi­mi kai­kis­sa ti­lan­teis­sa.
Mui­ta­kin on: ln, log2, sin, div jne.
ver­tai­lut
sym­bo­li kir­joi­ta
<<
<=
==
!=
>=
>>
pe­rus­lo­giik­ka
sym­bo­li  kir­joi­ta  huo­mau­tus
/\ja; myös and kel­paa
\/tai; myös or kel­paa
¬!ei; myös not kel­paa
FFFepä­to­si
TTTto­si
UUUmää­rit­te­le­mä­tön
-->pro­po­si­tio­naa­li­nen imp­li­kaa­tio
<->pro­po­si­tio­naa­li­nen ek­vi­va­lens­si
&&&&oi­ko­sul­ku-ja
||||oi­ko­sul­ku-tai
päät­te­ly
sym­bo­li  kir­joi­ta  huo­mau­tus
==>
<==
<=>sa­mais­taa U ja F
===ei sa­mais­ta U ja F

Ali­päät­te­ly aloi­te­taan subproof ja lo­pe­te­taan subend. (Ali)päät­te­lyn en­sim­mäi­seen kaa­vaan voi­daan vii­ta­ta sa­nal­la original. Ali­päät­te­lyn alus­sa ole­va original viit­taa edel­li­sen ta­son en­sim­mäi­seen kaa­vaan. (Ali)päät­te­ly voi­daan ra­joit­taa jon­kin ole­tuk­sen täyt­tä­viin ta­pauk­siin kir­joit­ta­mal­la sen eteen assume kaa­va ;.
kvant­to­rit
sym­bo­likir­joi­ta
x:AA x:
x; 0 ≤ x < y:     AA x; 0 <= x < y:
x:EE x:
x; x + 2 ≠ z: EE x; x+2 != z:

(sym­bo­lien ; ja : vä­li­sen osuu­den syn­tak­si on ra­joi­tet­tu)

Mis­tä lo­gii­kas­sa on ky­se
Teh­tä­viä lu­kuun 4

Kir­joi­ta al­le ko­ko­nais­lu­ku­jen lau­se­ke tai kaa­va ja klik­kaa nap­pia, niin saat DFA:n, jo­ka esit­tää si­tä. Kaa­vas­sa saa käyt­tää kaik­kia en­sim­mäi­sen ker­ta­lu­vun pre­di­kaat­ti­lo­gii­kan piir­tei­tä. Lau­sek­kees­sa tai kaa­vas­sa ei saa ol­la ker­to­las­ku­ja, jois­sa mo­lem­mis­sa osa­puo­lis­sa esiin­tyy muut­tu­ja. Toi­min­nois­sa div ja mod täy­tyy ja­ka­jan ol­la po­si­tii­vi­nen ko­ko­nais­lu­ku­va­kio. Muu­ten saa käyt­tää kaik­kia ta­van­omai­sia ko­ko­nais­lu­ku­jen toi­min­to­ja. Li­säk­si tar­jol­la on joi­ta­kin epä­ta­van­omai­sia toi­min­to­ja. Niit­ten va­li­koi­man saat sel­vil­le ko­kei­le­mal­la tyh­jää syö­tet­tä se­kä syö­tet­tä 0 0.
tai