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

3. Õàðàêòåðèçàöèÿ ôîðìóë àëãåáðû âûñêàçûâàíèé                    37


   Ìû íå áóäåì äîêàçûâàòü äàííóþ òåîðåìó. Óêàæåì òîëüêî, ÷òî íåîá-
õîäèìîñòü äàííîãî êðèòåðèÿ ñðàçó ñëåäóåò èç îïðåäåëåíèÿ ñåìàíòè÷å-
ñêîé ïðîòèâîðå÷èâîñòè (íåâûïîëíèìîñòè), à äîêàçàòåëüñòâî äîñòàòî÷-
íîñòè ìîæíî íàéòè â [22].
   Òàêèì îáðàçîì, ñîãëàñíî äàííîé òåîðåìå ìíîæåñòâî Γ èç ïîñëåäíå-
ãî ïðèìåðà íåâûïîëíèìî. Îòìåòèì, ÷òî ïóñòîé äèçúþíêò çäåñü ìîæåò
áûòü íàéäåí çíà÷èòåëüíî áûñòðåå:
             (1)   q        resp (p ∨ q, ¬ p)
             (2)   r        resp (p ∨ r, ¬ p)
             (3)   ¬q       resr (¬ p ∨ ¬ q, r)
             (4)   ∅        resq ((1), (3))
    Ýòî íàòàëêèâàåò íà ìûñëü, ÷òî ïðîöåññ ðåçîëþòèâíîãî âûâîäà ìîæ-
íî ïîïûòàòüñÿ îïòèìèçèðîâàòü. Äëÿ âûáîðà èç ñîâîêóïíîñòè âñåâîç-
ìîæíûõ ïàð äèçúþíêòîâ, èìåþùèõ ðåçîëüâåíòó, êîíêðåòíîé ïàðû,
îáåñïå÷èâàþùåé ñêîðåéøåå çàâåðøåíèå ïðîöåññà (íàõîæäåíèå ïóñòî-
ãî äèçúþíêòà), ïðèìåíÿþò ðàçëè÷íûå ýâðèñòè÷åñêèå ïðàâèëà, íàçû-
âàåìûå ñòðàòåãèÿìè ìåòîäà ðåçîëþöèé . Ðàçëè÷àþò ïîëíûå è íåïîë-
íûå ñòðàòåãèè. Ñòðàòåãèè ïåðâîãî òèïà ãàðàíòèðóþò ïîëó÷åíèå ïóñòî-
ãî äèçúþíêòà â ñëó÷àå, åñëè äàííîå ìíîæåñòâà äèçúþíêòîâ ïðîòèâîðå-
÷èâî. Òàêèå ñòðàòåãèè äîëæíû îáåñïå÷èâàòü, â êîíå÷íîì ñ÷¼òå, ïîðîæ-
äåíèå âñåõ ðåçîëüâåíò äàííîãî ìíîæåñòâà äèçúþíêòîâ Γ. Ñòðàòåãèè
âòîðîãî òèïà, íå ïîðîæäàÿ âñåõ ðåçîëüâåíò Γ, ìîãóò çàêîí÷èòü ðàáîòó,
îñòàâèâ âîïðîñ î âûâîäèìîñòè ïóñòîãî äèçúþíêòà áåç îòâåòà. Îäíàêî â
áîëüøèíñòâå ñëó÷àåâ ïðîòèâîðå÷èâîñòè Γ ñîîòâåòñòâóþùèå àëãîðèò-
ìû ïðèâîäÿò ê ðåçóëüòàòó çíà÷èòåëüíî áûñòðåå àëãîðèòìîâ ïåðâîãî
òèïà. Îòìåòèì, ÷òî íàèáîëåå òðóäî¼ìêîé îïåðàöèåé ìåòîäà ðåçîëþ-
öèé ÿâëÿåòñÿ íàõîæäåíèå ïàðû äèçúþíêòîâ ñ êîíòðàðíûì âõîæäåíèåì
íåêîòîðîé ïåðåìåííîé.
    Îïèñàííûé ìåòîä ìîæåò áûòü ïðèìåí¼í è äëÿ ïðîâåðêè ëîãè÷åñêî-
ãî ñëåäîâàíèÿ Γ ² A. Äåéñòâèòåëüíî, ñîãëàñíî ïðèíöèïó äåäóêöèè (ñì.
ñ. 24) Γ ² A ðàâíîñèëüíî Γ, ¬ A ² èëè ñåìàíòè÷åñêîé ïðîòèâîðå÷èâî-
ñòè ñîîòâåòñòâóþùåãî ìíîæåñòâà äèçúþíêòîâ. Ïîíÿòíî, ÷òî â äàííîì
ñëó÷àå ìåòîä ðåçîëþöèé åñòü âàðèàíò ìåòîä äîêàçàòåëüñòâà îò ïðî-
òèâíîãî: ïðåäïîëàãàÿ, ÷òî ëîãè÷åñêîå ñëåäîâàíèå íåâåðíî, ïðèõîäÿò ê
ïðîòèâîðå÷èþ.
Ïðèìåð 1.12. Ïðîâåðèì ìåòîäîì ðåçîëþöèé ñïðàâåäëèâîñòü ëîãè÷å-
ñêîãî ñëåäîâàíèÿ
            ¡   ¡           ¡        ¡             ¡   ¡
          p ¢(q ¢ r), r N s ¢ t, ¬ u ¢ s N ¬ t ² p ¢(q ¢ u) .
                              ¡   ¡
   Îòðèöàíèå ñëåäñòâèÿ ¬ (p ¢(q ¢ u)) ñ÷èòàåì íîâîé äîïîëíèòåëü-
íîé ãèïîòåçîé. Èñïîëüçóÿ ïðåäñòàâëåíèå èìïëèêàöèè ÷åðåç äèçúþíê-
öèþ è ïðàâèëà Äå Ìîðãàíà, ïðåäñòàâèì âñå ãèïîòåçû â âèäå ñîâîêóï-