4f Checker
SD editorn har en plug-in, 4f Checker, som du kan använda för att kontrollera om din härledning är matematiskt korrekt. Checkern formulerar varje steg i härledningen som ett matematiskt teorem och skickar detta till en automatisk teorembevisare som körs i molnet. Härledningen är korrekt, om varje steg i den är korrekt. Checkern ger en varning för varje steg i härledningen som den inte kunde bevisa att är korrekt.
Härledning med ett fel
Härledningen nedan innehåller ett fel, det andra steget är inte korrekt. Checkern visar ett "!" som varningstecken vid det felaktiga steget, och en bock vid de korrekta stegen.
Korrigerad härledning
Här har vi korrigerat det felaktiga steget. Checkern markerar nu varje steg som korrekt, så hela härledningen är korrekt.
Användning av checkern
Checkern gör en markering för varje steg i härledningen i kolumnen till höger. Checkern kan ställas inför olika situationer när den kontrollerar steget:
a) Checkern kan rapportera att den inte förstår steget i härledningen. Det kan finnas ett syntaxfel i steget, eller du kanske använder matematiska beteckningar som checkern inte känner till. Du bör då skriva om steget.
b) Checkern kan rapportera att steget är korrekt. Då är allt bra.
c) Checkern kan rapportera att den inte kunde bevisa steget. Det kan finnas olika orsaker till detta:
1. Checkern kan inte bevisa steget eftersom det är felaktigt. Du måste fixa felet.
2. Tiden som checkern har till sitt förfogande löper ut innan den kan hitta ett bevis. Om du ändå tror att steget är korrekt kan du försöka hjälpa checkern genom att dela upp steget i mindre steg.
3. Checkern vet inte tillräckligt mycket om matematiken bakom steget för att bevisa det. Försök att lägga till antaganden, fakta eller definitioner som skulle göra det enklare för checkern att bevisa steget.
Checkern är endast avsedd som hjälp vid kontroll av din härledning. I slutändan är det du själv som är ansvarig för att kontrollera att härledningen är korrekt. Checkern ger tips om hur man hittar fel och skapar en korrekt lösning.
Vad checkern kan bevisa
eMath-checkern använder ett antal olika automatiska system för teorembevisning parallellt för att försöka bevisa att ett steg är korrekt. Vart och ett av dessa system har alla sina speciella styrkor. De kan vara bra på att bevisa teorem inom vissa områden av matematiken, medan de kan vara ganska dåliga på andra områden. Därför beror checkerns effektivitet på vilket område inom matematiken som den kontrollerar och vilka automatiska systemen för teorembevisning som är tillgängliga för detta område.
Styrkor
Checkern är rätt bra på att bevisa härledningssteg inom följande områden av matematik.
- Polynom (ekvationer, olikheter, funktioner)
- Rationella uttryck (rationella aritmetiska och polynomialuttryck)
- Rotuttryck (potenser, kvadratrötter, rationella potenser)
- Logaritmer
- Exponenter
- Första ordningens logik
- Grundläggande trigonometri
Vissa av dessa områden kan kräva mer kraftfulla teorembevisare, som är tillgängliga för en extra avgift.
4f Checkerns användning
4f Checkern kan användas i 4f Studio och i 4f Note. Checkern kan användas på alla ställen där matematikverktyget används: i 4f-läroböcker när man löser uppgifter, i 4f anteckningsböcker och i 4f kursböcker. 4f Checkern kräver att användaren har en aktiv prenumeration på 4f Studio eller 4f Note.
Du kontrollerar en härledning genom att välja "kontroll" i checkerns meny. Det här startar kontrollprocessen. Checkern kontrollerar alla steg i härledningen parallellt med hjälp av tre eller fyra olika automatiska teorembevisare parallellt för varje steg. Checkern markerar varje steg med antingen en bock (steget är korrekt) eller ett utropstecken (när den inte hittade ett bevis). Checkern kan också indikera ett syntaxfel för ett steg som den inte förstår. Alternativet "ta bort markeringar" i menyn tar bort alla markeringar.
