Automaattinen tarkistus

Rakenteisten päättelyketjujen editoriin voi liittää lisäosan, jonka avulla voit tarkistaa, onko päättelyketjusi matemaattisesti oikein. Tarkistin muotoilee jokaisen päättelyketjun askeleen teoreemaksi, jonka se lähettää pilvipalvelimessa toimiville automaattisille teoreemantarkistimille. Päätelyketju on oikein, jos sen jokainen askel voidaan todistaa.

Virheellinen päättelyketju

Seuraava päättelyketju on virheellinen, sillä toisessa askeleessa on laskuvirhe. Tarkistin merkitsee huutomerkin "!" virheellisen askeleen kohdalle, ja merkin "٪" oikein tehtyjen askelten kohdalle.

Korjattu päättelyketju

Tässä virhe on korjattu. Tarkistin merkitsee kaikki askeleet oikein tehdyiksi, joten koko päättelyketju on oikein.
 

Chips by lamdogjunkie, www.flickr.com. CC BY 2.0

Tarkistimen käyttö

Tarkistin palauttaa jokaiseen askeleeseen sarakkeen oikeaan reunaan merkin.

  1. Tarkistin voi ilmoittaa, ettei se ymmärrä askelta, jolloin se pitää kirjoittaa uudelleen:

    1. Askeleessa voi olla syntaksivirhe, ja se pitää korjata.
    2. Tarkistin ei ymmärrä merkintätapaa. Tällöin pitää käyttää toisenlaista merkintätapaa-
  2. Tarkistin voi ilmoittaa askeleen oikeaksi. Askel on kunnossa.
  3. Tarkistin ymmärtää askeleen, muttei pysty todistamaan sitä.
    1. Askel voi olla virheellinen, jolloin sitä ei voi todistaa. Virhe pitää korjata
    2. Askel voi olla oikein, mutta tarkistin ei pysty todistamaan sitä käytettävissä olevassa ajassa. Sen voi yrittää pilkkoa pienempiin askeleisiin.
    3. Askel voi olla oikein, mutta tarkistimella ei ole riittävästi tietoa sen todistamiseen. Tällöin tarkistimelle pitää antaa lisää tietoa oletuksissa, johdettuina tosiasioina tai määritelminä.

Tarkistin on vain päättelyketjujen tarkistamisen apuväline. Se voi kuitenkin antaa hyviä vihjeitä siitä, miten ongelma ratkaistaan oikein.

Chips by lamdogjunkie, www.flickr.com. Licence CC BY 2.0

Mitä tarkistin voi todistaa?

Rakenteisten päättelyketjujen automaattinen tarkistin käyttää useita automaattisia teoreemantodistimia rinnakkain yrittäessään todistaa askeleen oikeaksi. Kaikilla teoreemantodistimilla on omat erityisalueensa, ja kukin voi olla hyvä yhdessä asiassa mutta huono toisessa. Tarkistimen tehokkuus riippuu siis siitä, onko juuri kyseiselle osa-alueelle tehokas todistin käytössä.

Osaamisalueet

Automaattinen tarkistin on varsin hyvä seuraavilla matematiikan osa-alueilla:

  1. polynomit (yhtälöt, epäyhtälöt, funktiot)
  2. rationaalilausekkeet(aritmeettiset ja polynomiset lausekkeet)
  3. juurilausekkeet(potenssit, neliöjuuret, murtopotenssit)
  4. logaritmit
  5. eksponenti
  6. ensimmäisen kertaluvun logiikka
  7. perustrigonometria

Jotkin näistä osa-alueista voivat vaatia tavallista tehokkaampia todistimia, jotka ovat käytössä lisämaksusta.