Formele logica
Assumptiecalculus
Bewijzen ingeven en controleren
Voorbeeld: de Snede
Kies ``Proof'' in het ``Insert'' menu:
en er verschijnt een leeg bewijs.
Je kan het bewijs dan beginnen invullen. Er zijn drie kolommen:
links de volgnummers (waar je niets aan kan en hoeft te veranderen),
in het midden de sequenten, en rechts de verantwoordingen.
Begin met de eerste regel gewoon in te tikken. Een turnstyle
maak je door eerst een | (pipe-symbool) en dan een - (minteken)
te typen:
Voor de Azerty-tikkers:
de pipe zit nogal eens onder Alt-Gr 1
|
Door op [Enter] te drukken, maak je een nieuwe regel.
Er verschijnt een nieuwe regel met volgnummer 2. De twee rode vierkantjes
geven aan dat er iets moet ingevuld worden (een formule en een verantwoording
in dit geval).
Typ de tweede regel op de plaats van het linkse rode vierkantje:
Druk op de [cursor rechts] toets ([Tab] gaat ook) om de verantwoording in te vullen
(prem) en gebruik weer [Enter] om een nieuwe lijn bij te maken.
Zo kan je verder gaan tot het bewijs af is:
De ontkenning maak je door gewoonweg not te typen; van zodra de cursor
ervan weg is verandert de not in het juiste symbool.
Het programma kent verder ook nog de operatoren &, xor,
or, => en <=>. Verder kan je de
kwantoren ``voor alle'' en ``er bestaat'' bekomen door forall en
exists te typen.
Met de [Tab] en [Shift Tab] toetsen kan je door het bewijs
wandelen.
Het bewijs controleren
Om het bewijs te controleren, duw je op de rechtermuisknop terwijl
de muis over het bewijs staat:
Met Verify line wordt alleen de regel waarop de muis staat gecontroleerd;
met Verify proof wordt het hele bewijs gecontroleerd.
Als je het bewijs uit de figuur intikt, zal je zie dat Sicecas klaagt
dat de symbolen geen type hebben. Alle symbolen moeten eerst gedeclareerd
worden (hoe je lege regels kan toevoegen wordt een beetje verderop uitgelegd):
Als er een fout in het bewijs zit, wordt de regel rood omkaderd en krijg
je een (al dan niet duidelijke) foutboodschap.
Geldige types zijn
List Formula Term Pred Var Const
Lijnen invoegen en verwijderen
Lege lijnen invoegen gaat door op [Enter] te drukken:
Merk op dat de verwijzingen naar de verschoven lijnen aangepast zijn.
Je kan de regel er weer uit gooien door op [Backspace] te drukken.
Op die manier is het niet mogelijk een lijn bovenaan het bewijs
in te voegen. Daarvoor kan je de muispijl ergens in de bovenste helft
van de eerste lijn plaatsen, op de rechter muisknop duwen en
Insert line in het Proof menu kiezen.
Om een lijn te verwijderen, maak je eerst de middelste en rechtse kolom leeg
(er blijft enkel een rood blokje over). Wanneer je dan op de [Backspace]
toets drukt, dan zal de lijn waarop de cursor staat verdwijnen.
Zoals te verwachten, worden alle verwijzingen naar verschoven lijnen
mee aangepast.
Lege formules
Soms moet aan de linkerkant van een turnstyle helemaal niets staan.
Als je de formule gewoon tikt, dus iets als
|-blablabla
dan wordt |- niet als een turnstyle herkend. Dat gebeurt enkel als
er twee argumenten aanwezig zijn. Maak dus eerst een dummy linkerargument:
d|-blablabla
en veeg dan de d weg. Er verschijnt een rood blokje links van
de turnstyle, wat normaal is.
Een andere truuk is
( )|-blablabla
intypen. Haakjes worden genegeerd door de bewijschecker, dus ``haakjes met
niets ertussen'' is hetzelfde als ``niets''. De haakjes mogen dus gewoon
blijven staan.
Commentaar
Commentaarlijnen kan je maken door niets in de rechterkolom te zetten en
de commentaar in de middelste kolom tussen aanhalingstekens:
Predikaatlogica
Vrije variabelen
Om uit te drukken dat x niet vrij voorkomt in L typ je
|-not(x in freevar(L))
Om uit te drukken dat x niet voorkomt in L typ je
|-not(x in vars(L))
Om uit te drukken dat L2 onstaat door in L1 alle vrije voorkomens van
x te vervangen door t, typ je
|-L2=subst(t,x,L1)
Merk op dat
|-subst(t,x,L1)=L2
niet zal gematcht worden (tenzij je daar zelf bewijsregels voor zou
gaan toevoegen natuurlijk).
Een overzicht van de meest gebruikte regels uit de substitutierekening
samen met twee voorbeeldbewijzen kan je in pdf
of postscript downloaden.
Terug