1300739940

Logika na co dzień

•    powtórzenia wyrażeń występujących w alternatywach (np. (A V A V B) można zastąpić przez równoważną formułę (A V Bj),

•    powtórzenia wyrażeń występujących w koniunkcjach (np. (A A A A B) można zastąpić przez równoważną formułę (A A B)).

Dla przykładu rozważmy formułę: (^-,(p A ~^,q) V (p => r)) V (r o —»s). Jej sprowadzenie do postaci klauzulowej może składać się z kroków:

•    ((^_,P V -■-'g) V (p => r)) V (r o —>s),

•    ((“'p V —-fj) V (-*p V r)) V(ro -*s),

•    (->p V V ~>p V r) V ~<s),

•    (-'p V q V -'p V r) V (r^ ^-is),

•    (->p    V q    V    —>p    V r) V ((t V —-s) A (r V ^-,-,s)),

•    (->p    V q    V    ^p    V r) V ((->r V —*s) A (r V s)),

•    (->p V g V r) V ((t V —*s) A (r V s)),

•    (~'p    V ^    V    r V    t V ->s) A (-'p V ^ V r V r V    s),

•    (->p    V g    V    r V    -r V —«s) A (-*p V ^ V r V s).

Wynikową formułę można z łatwością uprościć zauważając, że pierwsza klauzula ma zawsze wartość prawda (ponieważ zawiera alternatywę r V t):

•    1 A (-’p V q V r V s), czyli:

•    (-'p V ^ V r V s).

5.3. Metoda rezolucji

Metoda rezolucji wykorzystuje zasadę dowodzenia przez doprowadzanie do sprzeczności.

Metodę rezolucji wprowadził John Alan Robinson w 1965 roku. Była ona jednak stosowana już w XIX wieku, pod inną nazwą i w zakresie ograniczonym do formuł wybranej postaci. Wykorzystywał ją Charles Lutwidge Dodgson, znany także jako Lewis Carroll, autor m.in. Alicji w krainie czarów. W jego podręczniku Symbolic Logic (1896 r.) metoda ta nosi nazwę method of underscoring.

Metoda rezolucji jest w swojej istocie oparta na przechodniości implikacji, czyli na regule mówiącej że:

19