293017405

Etap 9 - standaryzacja zmiennych

->Standaryzacja zmiennych w niezależnych klauzulach.

-^Każdej zmiennej można nadać inną nazwę, co nie zmieni znaczenia logicznego, a zapobiega myleniu zmiennych podczas dowodzenia.

Przykład konwersji

Vx:lRoman(x) aknow(x,Marcu.¹;)] —»[hate(x,Caesar) v (Vy: 3z : haie(y,z) —>thinkcrazy(x,>'))] i (etap 1)

V*: ~{Roman(x) a know(x,Marcuś)] v [hate(x,Caesar) v (Vy: -i(3z: hale(y, z)) v thinkcrazy(x, y))]

| (etap 2)

V*: [—\Roman(x) v —tknow(x,Marcus)] v [/tare(x, Caesar) v (Vy: Vz: —\hate( y, z) v thinkcrazy(x, y))] i (etap 4)

: Vy: Vz:    v —>know(x,Marcus)\ v

[/ra/e(jt, Caesar) v (—ihate(y, z) v thinkcrazy(x, y))]

| (etap 6)

[—v -i&wowf*, Marcuj)] v [/ta/e(.x,Caesar) v (—iha!e(y, z) v thinkcrazy(x, y))] | (etap 7)

—iRoman(x) v —\know{x, Marcus) v hate(x,Caesar) v —ihate(y, z) v thinkcrazy(x, y)

36

18