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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

D =
_
i∈I
x
σ
i
i
,
I x
i
i = 1, 2, . . . σ
i
∈ { , }
x = x x = ¬ x I = ∅ D = ∅ ∅
X
x A B
A ∨ x, B ∨ ¬ x ² A ∨ B (RR)
D
1
D
2
D
1
= A ∨ x D
2
= B ∨ ¬ x
x A ∨B
D
1
D
2
x
A ∨ B = res
x
(D
1
, D
2
)
x D
1
D
2
D
1
D
2
res (D
1
, D
2
)
res (x, ¬ x)
def
= ∅ res (D
1
, D
2
) 6= ∅
D
1
N D
2
∼ D
1
N D
2
N res (D
1
, D
2
).
3. Õàðàêòåðèçàöèÿ ôîðìóë àëãåáðû âûñêàçûâàíèé                               35


âûâîäèìîñòè íåêîòîðîé ôîðìóëû èç äàííîãî ìíîæåñòâà ôîðìóë19 .
   Êàê áûëî óêàçàíî, äèçúþíêòîì íàçûâàåòñÿ äèçúþíêöèÿ êîíå÷íîãî
÷èñëà ïðîïîçèöèîíàëüíûõ ïåðåìåííûõ èëè èõ îòðèöàíèé, ò.å. ôîðìóëà
âèäà                           _
                          D =     xσi i ,
                                      i∈I

ãäå I  êîíå÷íîå ïîäìíîæåñòâî íàòóðàëüíûõ èíäåêñîâ, xi ,
i = 1, 2, . . .  ïðîïîçèöèîíàëüíûå ïåðåìåííûå, σi ∈ {1, 0} è,
êàê îáû÷íî, x1 = x, x0 = ¬ x. Åñëè I = ∅, òî èìååì D = ∅, ãäå ∅ 
ïóñòîé äèçúþíêò , ýêâèâàëåíòíûé êîíñòàíòå 0.
   Â ñèëó êîììóòàòèâíîñòè è àññîöèàòèâíîñòè êîíúþíêöèè, ÊÍÔ
ìîæíî ïðåäñòàâèòü ïðîñòî ñîâîêóïíîñòüþ äèçúþíêòîâ. Ñ äðóãîé ñòî-
ðîíû, ñîãëàñíî ïðèíöèïó äåäóêöèè (ñì. ñ. 24), êðèòåðèåì íåâûïîë-
íèìîñòè ìíîæåñòâà äèçúþíêòîâ ÿâëÿåòñÿ ëîãè÷åñêîå ñëåäîâàíèå èç
íåãî ïóñòîãî äèçúþíêòà. Èäåÿ ìåòîäà ðåçîëþöèé ñîñòîèò â ïðåäñòàâ-
ëåíèè äàííîé ôîðìóëû èëè ëîãè÷åñêîãî ñëåäîâàíèÿ â âèäå ñîâîêóï-
íîñòè äèçúþíêòîâ ñ äàëüíåéøèì ïîðîæäåíèåì èç ïîëó÷åííîãî ìíîæå-
ñòâà ðàçëè÷íûõ ëîãè÷åñêèõ ñëåäñòâèé äî òåõ ïîð, ïîêà íå áóäåò ëèáî
ïîëó÷åí ïóñòîé äèçúþíêò, ëèáî óñòàíîâëåíà íåâîçìîæíîñòü åãî ïîëó-
÷åíèÿ.
   Äëÿ ïîðîæäåíèÿ äèçúþíêòîâ èñïîëüçóåòñÿ ïðàâèëî 9 ïðèìåðà 1.6,
ïðèìåíÿåìîå äëÿ ñëó÷àÿ, êîãäà X  ïðîïîçèöèîíàëüíàÿ ïåðåìåííàÿ
(óäîáíåå å¼ îáîçíà÷àòü êàê x), à A è B  äèçúþíêòû.  ýòîì ñëó÷àå
îíî èìååò âèä
                       A ∨ x, B ∨ ¬ x ² A ∨ B                (RR)
è íàçûâàåòñÿ ïðàâèëîì ðåçîëþöèé .
   Åñëè äèçúþíêòû D1 è D2 èìåþò âèä D1 = A ∨ x è D2 = B ∨ ¬ x
ãäå x  íåêîòîðàÿ ïðîïîçèöèîíàëüíàÿ ïåðåìåííàÿ, òî ôîðìóëó A ∨ B
íàçûâàþò ðåçîëüâåíòîé äèçúþíêòîâ D1 è D2 ïî ïåðåìåííîé x, ÷òî
çàïèñûâàþò A ∨ B = resx (D1 , D2 ). Ïîíÿòíî, ÷òî ðåçîëüâåíòà ñàìà ÿâ-
ëÿåòñÿ äèçúþíêòîì. Âõîæäåíèå ïåðåìåííîé x â äèçúþíêòû D1 è D2
íàçûâàþò êîíòðàðíûì . Ðåçîëüâåíòó äèçúþíêòîâ D1 è D2 ïî íåêîòî-
ðîé êîíòðàðíîé ïåðåìåííîé îáîçíà÷àþò res (D1 , D2 ). Ïî îïðåäåëåíèþ
                         def
ïîëàãàþò res (x, ¬ x) = ∅. Åñëè res (D1 , D2 ) 6= ∅, òî äîáàâëåíèå
ê äèçúþíêòàì-îñíîâàíèÿì ïðàâèëà ðåçîëþöèé äèçúþíêòà-ñëåäñòâèÿ
ïðèâîäèò ê ýêâèâàëåíòíîé êîíúþíêöèè:

                    D1 N D2 ∼ D1 N D2 N res (D1 , D2 ).
 19 Ðîáèíñîí Äæ.À. Ìàøèííî-îðèåíòèðîâàííàÿ ëîãèêà, îñíîâàííàÿ íà ïðèíöèïå
ðåçîëþöèè / Êèáåðíåòè÷åñêèé ñáîðíèê (Íîâàÿ ñåðèÿ), âûï. 7.  Ì.: Íàóêà, 1970. 
Ñ. 194218. Íàçâàíèå ìåòîäà ïðîèñõîäèò îò àíãë. resolution  ðàçðåøåíèå, ðàçðå-
øàþùàÿ ñïîñîáíîñòü.

Страницы