Исчисления высказываний классической логики. Гуров С.И. - 38 стр.

UptoLike

ВУЗ: 

МГУ | Москва

Составители: 

Рубрика: 

Γ
Γ = { ¬ p ∨ ¬ q ∨ r, ¬ r ∨ ¬ s ∨ t, u ∨ s, u ∨ ¬ t, p, q, ¬ u } .
Γ
¬ q ∨ r res
p
(¬ p ∨ ¬ q ∨ r, p)
r res
q
((8), q)
¬ r ∨ t ∨ u res
s
(¬ r ∨ ¬ s ∨ t, u ∨ s)
¬ r ∨ u res
e
((10), u ∨ ¬ t)
u res
r
((9), (11))
∅ res((12), ¬ u)
Γ
¬ x
1
∨ . . . ∨ ¬ x
m
∨ y ∼ x
1
N . . . N x
m
¡
¢
y ,
Γ
p D ∨ ¬ p
Γ D = res
p
(D ∨ ¬ p, p)
Γ = { p ∨ ¬ r ∨ ¬ t, q, r, t ∨ ¬ p ∨ ¬ r, t ∨ ¬ q, ¬ p ∨ ¬ q ∨ ¬ r } .
Γ
38                                 Ãëàâà 1. Êëàññè÷åñêàÿ àëãåáðà ëîãèêè


íîñòè äèçúþíêòîâ Γ. Ïîëó÷èì

       Γ = { ¬ p ∨ ¬ q ∨ r, ¬ r ∨ ¬ s ∨ t, u ∨ s, u ∨ ¬ t, p, q, ¬ u } .

Ñòðîèì ðåçîëþòèâíûé âûâîä (îïóñêàÿ ñïèñîê ýëåìåíòîâ Γ):
         (8)    ¬q ∨ r              resp (¬ p ∨ ¬ q ∨ r, p)
         (9)    r                   resq ((8), q)
         (10) ¬ r ∨ t ∨ u           ress (¬ r ∨ ¬ s ∨ t, u ∨ s)
         (11) ¬ r ∨ u               rese ((10), u ∨ ¬ t)
         (12) u                     resr ((9), (11))
         (13) ∅                     res((12), ¬ u)
   Ïîëó÷åí ïóñòîé äèçúþíêò, ÷òî ñâèäåòåëüñòâóåò î ïðîòèâîðå÷èâîñòè
ìíîæåñòâà Γ è ñïðàâåäëèâîñòè óñòàíàâëèâàåìîãî ëîãè÷åñêîãî ñëåä-
ñòâèÿ.
   Ïîíÿòíî, ÷òî ïîñêîëüêó ïðîâåðêà âûïîëíèìîñòè òîé èëè èíîé ôîð-
ìóëû ÿâëÿåòñÿ ïåðåáîðíîé çàäà÷åé, òî ìåòîä ðåçîëþöèé áóäåò ýôôåê-
òèâåí ëèøü â îïðåäåë¼ííûõ ÷àñòíûõ ñëó÷àÿõ. Âàæíåéøèì èç íèõ ÿâ-
ëÿåòñÿ ñëó÷àé õîðíîâñêèõ äèçúþíêòîâ . Õîðíîâñêèìè íàçûâàþò äèçú-
þíêòû, ñîäåðæàùèå íå áîëåå îäíîé ïåðåìåííîé áåç îòðèöàíèÿ. Åñëè
õîðíîâñêèé äèçúþíêò ñîäåðæàò òàêóþ ïåðåìåííóþ, òî îí íàçûâàåòñÿ
òî÷íûì ; â ïðîòèâíîì ñëó÷àå äèçúþíêò íàçûâàþò íåãàòèâíûì . Ïî-
ñêîëüêó
                                                       ¡
             ¬ x1 ∨ . . . ∨ ¬ xm ∨ y ∼ x1 N . . . N xm ¢ y ,
òî÷íûé õîðíîâñêèé äèçúþíêò íåðåäêî âûðàæàåò íåêîòîðîå ñëåäîâà-
íèå. Äèçúþíêò, ñîñòîÿùèé èç åäèíñòâåííîé ïðîïîçèöèîíàëüíîé ïåðå-
ìåííîé (áåç îòðèöàíèÿ) íàçîâ¼ì óíèòàðíûì ïîçèòèâíûì äèçúþíê-
òîì .
   Äëÿ õîðíîâñêèõ äèçúþíêòîâ ìåòîä ðåçîëþöèé ìîæåò áûòü ñâåä¼í ê
ñëåäóþùåìó ïðîñòîìó àëãîðèòìó. Íà êàæäîì øàãå àëãîðèòìà èç ìíî-
æåñòâà äèçúþíêòîâ Γ âûáèðàåòñÿ óíèòàðíûé ïîçèòèâíûé äèçúþíêò,
ñîñòîÿùèé èç íåêîòîðîé ëèòåðû p è äèçúþíêò âèäà D ∨ ¬ p. Çàòåì â
Γ ïîñëåäíèé äèçúþíêò çàìåíÿåòñÿ ðåçîëüâåíòîé D = resp (D ∨ ¬ p, p).
Ïðîäåìîíñòðèðóåì ðàáîòó àëãîðèòìà íà ïðèìåðå.
Ïðèìåð 1.13. Ïðîâåðèòü íåâûïîëíèìîñòü ìíîæåñòâà õîðíîâñêèõ äèçú-
þíêòîâ

     Γ = { p ∨ ¬ r ∨ ¬ t, q, r, t ∨ ¬ p ∨ ¬ r, t ∨ ¬ q, ¬ p ∨ ¬ q ∨ ¬ r } .

   Øàãè àëãîðèòìà áóäåì îïèñûâàòü ñòðîêàìè òàáëèöû, ñîäåðæàùåé
â ñâîèõ ñòîëáöàõ ýëåìåíòû ìíîæåñòâà Γ. Ïåðåìåííóþ, ïî êîòîðîé îá-
ðàçóåòñÿ ðåçîëüâåíòà áóäåì ïîä÷¼ðêèâàòü.

Страницы