Tremetoden i predikatlogikk

Question 1

Hva er trereglene for universell kvantor?

Answer 1

Hvis en åpen sti inneholder en linje med formelen Ava, kan formelen a føyes til som en ny linje i alle åpne stier under linjen, men med alle frie forekomster av individvariabelen v i a byttet ut med en og samme individkonstant k (fortrinnsvis en individkonstant som ikke finnes)

Eks:
1 Ax(Fx->Gx) P
2 Fa -> Ga 1 A

Vi sjekker ikke linjen vi anvender regelen på

Question 2

Hva er trereglene for eksistensiell kvantor?

Answer 2

Hvis en åpen sti inneholder en usjekket linje med formelen Ex(Fx ^ Gx): Sjekk linjen og føy til formelen (Fx ^ Gx) som en ny linje i alle åpne stier under den sjekkede linjen, men med alle frie forekomster av individvariabelen x byttet ut med én og samme individkonstant k som IKKE allerede finnes i stien

Eks:
1 Ex(Fx ^ Gx). P
2 Fb ^ Gb. 1 E

Siden man skal bruke en individkonstant som ikke allerede finnes, er det lurt å begynne med eksistensiell kvantor før universell

Question 3

Hva er treregelen for negert universell kvantor?

Answer 3

Hvis en åpen sti inneholder en usjekket linje med formelen : notAx(Fx->Gx)
Sjekk linjen og føy til Exnot(Fx->Gx) som en ny linje i alle åpne stier under den sjekkede linjen (uten å modifisere variabler).
eks:
1 notAx(Fx->Gx) P
2 Exnot(Fx->Gx) 1A

Question 4

Hva er treregelen for negert eksistensiell kvantor?

Answer 4

Hvis en åpen sti inneholder en usjekket linje med formelen notEx(Fx^Gx):
Sjekk linjen og føy til Axnot(Fx^Gx) som en ny linje i alle åpne stier under den sjekkede linjen (uten å modifisere variabler).

eks:
                     1              notEx(Fx^Gx)       P
                     2             Axnot(Fx^Gx)       1 E

Question 5

Gi 3 eksempler på operatorer som ikke splitter stier

Answer 5

Konjunksjoner, negerte disjunksjoner og negerte kondisjonaler