Formele logica

Assumptiecalculus

Bewijsregels opladen

Afhankelijk van de logica waarin je wil gaan werken, kan je verschillende bewijsregels opladen. Ik heb wat voorgedefinieerde verzamelingen bewijsregels voorzien:

propc Zes basis-bewijsregels uit de propositielogica.
propcc Uitgebreide regels uit de propositielogica.
Enige verschil met Flobes is dat de regels DefA en DefC uiteenvallen in DefAimpl, DefAor, DefCimpl en DefCor.
PENDING: DeRe1 en DeRe2 zitten er nog niet in.
predc Vijf basis-bewijsregels uit de predikatenlogica.

De makkelijke methode

Eerste variant: typ het bewijs in, druk er met de rechtermuisknop op, kies eventueel de Proof knop onderaan het menu, kies het Rules menu en kies voor Load xxx waarbij xxx je favoriete verzameling regels is. De regels worden aan de reeds ingelezen regels toegevoegd. De oude regels verdwijnen dus niet, en door meerdere keren regels op te laden kan je meerdere verzamelingen regels tegelijkertijd actief hebben.

Tweede variant: typ het bewijs in en verifieer het (dit wordt verderop in meer detail besproken). Als de bewijschecker op een fout botst (bijvoorbeeld omdat er geen regels geladen zijn), verschijnt een venster met een foutboodschap erin, waar ook zo'n Rules knop staat. Laad je favoriete verzameling(en) regels en duw op OK. Nu kan je het bewijs opnieuw verifiëren.

De moeilijke methode

Deze methode kan je gebruiken als je eigen verzamelingen bewijsregels wilt opladen (die natuurlijk niet in de menu's van hiervoor voorkomen).

De bewijsregels die de proof-checker zal gebruiken, moeten in een variabele genaamd rules staan. Dus met

propc [Enter] load [Enter] worden de bewijsregels opgeladen:

Zoals je kan zien, is dit niets meer of niets minder dan een verzameling van bewijsregels.
Als je alleen maar deze regels wilt gebruiken, kan je nu al rules [Enter] sto [Enter] typen. Meestal zal je ook wel andere regels willen gebruiken, bijvoorbeeld die van propcc. Tik dus propcc [Enter] load [Enter] Nu staan de regels uit propc en die uit propcc onder elkaar op de stapel. We kunnen hier één grote verzameling van maken met de union operator; typ union [Enter] om de volgende (lange) uitdrukking te bekomen:

Als we dit in de rules variabele zouden stoppen, zal de proof-checker verderop in de soep draaien, want die verwacht dat er enkel één verzameling in zit, en geen rare uitdrukkingen met unies erin en zo. Dus rekenen we de unie uit door ; [Enter] te tikken.
PENDING: dit geeft een errormelding No definition for same() in formula.ProofRule op de console (kan geen kwaad)
Eventueel kan je nu nog andere bewijsregels opladen, weer de unie nemen, enzovoort.
Uitendelijk prop je alles in de rules variabele met rules [Enter] sto [Enter]

Terug