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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

p ∨ ¬ r ∨ ¬ t q r t ∨ ¬ p ∨ ¬ r t ∨ ¬ q ¬ p ∨ ¬ q ∨ ¬ r
p ∨ ¬ r ∨ ¬ t q r t ∨ ¬ p ∨ ¬ r t ¬ p ∨ ¬ q ∨ ¬ r
p ∨ ¬ t q r t ∨ ¬ p ∨ ¬ r t ¬ p ∨ ¬ q ∨ ¬ r
p ∨ ¬ t q r t ∨ ¬ p ∨ ¬ r t ¬ p ∨ ¬ r
p ∨ ¬ t q r t ∨ ¬ p ∨ ¬ r t ¬ p
p q r t ∨ ¬ p ∨ ¬ r t ¬ p
p q r t ∨ ¬ p ∨ ¬ r t ∅
∆
p D ∨ ¬ p
Γ
A N B ² A N x ∨ B N ¬ x (CR)
A B
res
x
(A N x, B N ¬ x) = A ∨ B , res (x, ¬ x) = ∅ ,
x
K
1
K
2
res (K
1
, K
2
) 6= ∅
K
1
∨ K
2
∼ K
1
∨ K
2
∨ res (K
1
, K
2
) ,
3. Õàðàêòåðèçàöèÿ ôîðìóë àëãåáðû âûñêàçûâàíèé                         39

   1    p ∨ ¬r ∨ ¬t     q    r    t ∨ ¬p ∨ ¬r    t ∨ ¬q   ¬p ∨ ¬q ∨ ¬r
   2    p ∨ ¬r ∨ ¬t     q    r    t ∨ ¬p ∨ ¬r       t     ¬p ∨ ¬q ∨ ¬r
   3       p ∨ ¬t       q    r    t ∨ ¬p ∨ ¬r       t     ¬p ∨ ¬q ∨ ¬r
   4       p ∨ ¬t       q    r    t ∨ ¬p ∨ ¬r       t       ¬p ∨ ¬r
   5       p ∨ ¬t       q    r    t ∨ ¬p ∨ ¬r       t          ¬p
   6          p         q    r    t ∨ ¬p ∨ ¬r       t          ¬p
   7          p         q    r    t ∨ ¬p ∨ ¬r       t           ∅

   Àëãîðèòì çàêîí÷èò ñâîþ ðàáîòó çà êîíå÷íîå ÷èñëî øàãîâ âíå çàâè-
ñèìîñòè îò âûáîðà ïàðû äèçúþíêòîâ íà êàæäîì øàãå. Â êîíöå ðàáîòû
áóäåò ïîëó÷åíû ëèáî ïóñòîé äèçúþíêò, ëèáî ìíîæåñòâî ∆, íå ñîäåð-
æàùåå äèçúþíêòîâ âèäà p è D ∨ ¬ p.  ïåðâîì ñëó÷àå èñõîäíîå ìíî-
æåñòâî äèçúþíêòîâ Γ íåâûïîëíèìî, à âî âòîðîì, êàê ìîæíî ïîêàçàòü,
ïîñòðîèâ ñîîòâåòñòâóþùóþ ìîäåëü  âûïîëíèìî.
   Ìåòîä ðåçîëþöèé, ÿâëÿÿñü ýôôåêòèâíîé àëüòåðíàòèâîé òðàäèöèîí-
íûì ïðàâèëàì óìîçàêëþ÷åíèé, øèðîêî èñïîëüçóåòñÿ ïðè àâòîìàòè÷å-
ñêîì âûâîäå òåîðåì â ôîðìàëüíûõ èñ÷èñëåíèÿõ. Äàííûé ìåòîä, î÷å-
âèäíî, ÿâëÿåòñÿ ÷èñòî ñèíòàêñè÷åñêèì, íå èñïîëüçóþùèì èñòèííîñò-
íûå îöåíêè ðàññìàòðèâàåìûõ ôîðìóë è ïîäôîðìóë.
   Äâîéñòâåííûì ïðàâèëîì ê ìåòîäó ðåçîëþöèé ÿâëÿåòñÿ ìåòîä ñî-
ãëàñèÿ. Îí îñíîâàí íà ñëåäóþùåì ïðàâèëå ñîãëàñèÿ :

                        ANB ² ANx ∨ B N¬x                          (CR)

â ñëó÷àå, êîãäà A è B  êîíúþíêòû. Íà îñíîâå äàííîãî ïðàâè-
ëà ñôîðìóëèðóåì ìåòîä, äâîéñòâåííûé ê ìåòîäó ðåçîëþöèé, ïîçâîëÿ-
þùèé óñòàíàâëèâàòü òîæäåñòâåííóþ èñòèííîñòü ÄÍÔ. Ïîëîæèì ïî
îïðåäåëåíèþ

resx (A N x, B N ¬ x) = A ∨ B ,   res (x, ¬ x) = ∅ (åäèíè÷íûé êîíúþíêò) ,

ãäå x  íåêîòîðàÿ ïðîïîçèöèîíàëüíàÿ ïåðåìåííàÿ.
   Ïóñòü K1 è K2  êîíúþíêòû è res (K1 , K2 ) 6= ∅. Äîáàâëå-
íèå ê êîíúþíêòàì, ñîñòàâëÿþùèì çàêëþ÷åíèå ïðàâèëà ñîãëàñèÿ,
êîíúþíêòà-îñíîâàíèÿ ïðèâîäèò ê ýêâèâàëåíòíîé äèçúþíêöèè

                  K1 ∨ K2 ∼ K1 ∨ K2 ∨ res (K1 , K2 ) ,

âûðàæàþùåé ïðàâèëî îáîáù¼ííîãî ñêëåèâàíèÿ 21 .
  21 Ñì. Þ.È. Æóðàâë¼â. ¾Àëãîðèòìû ïîñòðîåíèÿ ìèíèìàëüíûõ äèçúþíêòèâíûõ
íîðìàëüíûõ ôîðì äëÿ ôóíêöèé àëãåáðû ëîãèêè¿ / Äèñêðåòíàÿ ìàòåìàòèêà è ìà-
òåìàòè÷åñêèå âîïðîñû êèáåðíåòèêè, ò. I.  Ì.: Íàóêà, 1974.  Ñ. 67-98

Страницы