Ratkaisun tekeminen oikein tarkistimen avulla

Tässä näytetään, miten  tehtävä ratkaistaan oikein käyttäen tarkistinta apuna. Tehtävänä on ratkaista rationaaliyhtälö.

Askeleet oikein mutta epätäydellinen ratkaisu

Automaattinen tarkistin pyrkii todistamaan kaikki ratkaisun askeleet oikeiksi erikseen. Oikealla on rakenteinen päättelyketju, jossa kaikki askeleet ovat oikein, mutta ratkaisu on epätäydellinen. Siinä ei ole vastausta. Tarkistin on todistanut alipäättelynä olevan nimittäjän jaon tekijöihin oikeaksi.

chekckeresimvajaa

Virheellinen ratkaisu

Päättelyketju oikealla on täydennetty niin, että tehtävään on saatu ratkaisu. Ratkaisu ei ehkä ole oikein, koska tarkistin ei ole pystynyt todistamaan kahta askelta. Huolellinen tarkastelu osoittaa, että jälkimmäisessä näistä on merkkivirhe. Kyseinen askel ja kaikki sen jälkeen tulevat askeleet pitää korjata.

chekckeresimvirhe

Perustelut ja oletukset

Oikealla olevassa päättelyketjussa merkkivirhe on korjattu. Jäljelle jää edelleen kaksi askelta, joita tarkistin ei pysty todistamaan. Ensimmäistä ei voi todistaa oikeaksi, koska lauseke, jolla kerrotaan voi olla nolla. Jälkimmäisessä askeleessa perustelussa sanotaan, että binomi ei voi olla nolla. Tarkistin ei kuitenkaan näe syytä, miksei se voisi olla nolla. Nämäkin askeleet voidaan todistaa lisäämällä oletus, jonka mukaan kyseiset nimittäjissä esiintyvät lausekkeet eivät saa olla nollia.

chekckeresimeioletuksia

Oikea ratkaisu

Viimein on saatu oikealla oleva ratkaisu. Koska kaikki oletusten kanssa ristiriidassa olevat  yhtälön ratkaisut on poistettu ja tarkistin pystyy todistamaan kaikki askeleet,  ratkaisu on oikein.

chekckeresimoikein