Formele logica
Semantische tableaus
Een tableau wordt opgebouwd uit een sequent van de vorm
a1,a2,...,an |>
b1,b2,...,bn
waarbij de a'tjes en de b'tjes formules zijn:
Het driehoekje maak je door gewoon een | (pipe) en een >
te typen.
Door midden van een aantal reductieregels op operatoren groeit de boom.
Klik bijvoorbeeld met de rechtermuisknop op de meest linkse &:
Kies voor Reduce in tableau om de reductie door te voeren:
We pakken nu de middenste & op analoge wijze aan:
Enzovoort:
De twee overblijvende not operatoren kan je ook wegkrijgen door er
met de rechtermuis op te klikken en weer Reduce in tableau
te kiezen. Hiermee is het tableau volledig gereduceerd.
PENDING: Het programma duidt nog niet
aan dat een tak sluit ...
Je kan overigens ook op de lijnen van het tableau met de rechterknop
klikken om van een `splitsing' een `rechtdoor' te maken en
omgekeerd.
Terug