Hur man använder checkern

Här visar vi hur checkern kan användas för att lösa ett matematiskt problem. Uppgiften är att lösa en rationell ekvation.

Ofullständig lösning

4f Checkern försöker bevisa varje steg i lösningen var för sig. Den strukturerade härledningen till höger har korrekta steg men den är ofullständig. Svaret på problemet saknas. Faktoriseringen av nämnaren i ekvationens högra led är skriven som en delhärledning, och checkern kan bevisa den.

checkerexincompleteb

Felaktig lösning

Vi lägger till svaret till härledningen.

Checkern kan inte bevisa varje steg i härledningen till höger. Vi måste noggrant studera de steg som inte kan bevisas. Vi hittar ett fel vid den andra varningen: termerna som nämns i motiveringen skall subtraheras, inte adderas. Det här steget och alla efterföljande steg måste korrigeras.

checkerexincorrectb

Motiveringar och antaganden

Vi korrigerar teckenfelet.

Det finns fortfarande två steg som checkern inte kan bevisa. Det första är steget där båda leden i ekvationen multipliceras med nämnarna. Checkern kan inte bevisa det här, eftersom vi inte kan veta om uttrycket som vi multiplicerar med är lika med noll. I det andra steget med en varning säger motiveringen att en av ekvationerna inte kan vara sann, eftersom nämnaren då skulle vara lika med noll. Checkern ser dock ingen orsak till varför nämnaren inte skulle kunna vara lika med noll.

checkerexnoassumptionsb

Korrekt lösning

Vi lägger till antaganden som informerar checkern att nämnarna är olika noll.

Nu kan checkern bevisa varje steg i härledningen. Lösningen är korrekt.

checkerexcompleteb