Formele logica
Assumptiecalculus
Zels bewijsregels maken
Voorbeeld: de ZeBe regel
Tik de regel in op de gebruikelijke manier:
Bewaar het bewijs:
Merk op dat de bestandsnaam moet overeenkomen met de naam die je aan
de regel wil geven. De bewijschecker kijkt zelfs niet naar
de ZeBe(3) als dit bewijs als regel wordt gebruikt:
de naam wordt uit de bestandsnaam afgeleid en het aantal premissen
is het aantal regels waar prem als verantwoording bij staat.
Alleen als je de bewijsregel zelf gaat verifiëren (zie verder),
wordt de ZeBe(3) door de bewijschecker bekenen (net als in elk
andeer gewoon bewijs).
Vanaf nu kan je de ZeBe regel in eigen bewijzen gaan gebruiken.
Bewijsregels verifiëren
Je kan natuurlijk bewijsregels bijmaken zoveel je maar wil, maar
om te controleren of je bewijsregels een beetje betrouwbaar zijn,
kan je ze ook bewijzen. Als je de oude ZeBe regel vervangt door
(typ weer "ZeBe" [Enter] save om de nieuwe versie van de
regel actief te maken) dan werkt alles als voorheen:
andere bewijzen kunnen nog steeds van de ZeBe regel gebruik maken
(precies zoals in onze eerste versie zonder bewijs van de regel zelf).
Er is echter een interessant verschil: je kan de bewijsregel zelf
verifiëren (door, zoals altijd, Verify Proof in het
menu te kiezen dat verschijnt als je op de rechtermuisknop duwt).
Op die manier kan je er zeker van zijn dat bewijzen die onze
ZeBe regel gebruiken net zo goed met de A en R regels
kunnen gemaakt worden.
Hier kan je ook zien dat de bewijschecker niet kijkt naar de verantwoording
van de laatste lijn om de naam of het aantal argumenten van de regel
te bepalen (de regel heet niet R en er is maar één
premisse voor nodig).
Terug