Математическая логика и теория алгоритмов. Сергиевская И.М. - 20 стр.

     Без доказательства приведем следующую теорему.

     Теорема. Если из формулы A получено множество Δ предложений, то
формула A тождественно ложна тогда и только тогда, когда множество Δ
невыполнимо.

     До сих пор мы пользовались только одним правилом вывода – Modus ponens.
В других исчислениях высказываний имеют место и другие правила вывода.

                                                     ′                ′
     Правило резолюций. Даны предложения: С1 = P ∨ C1 , С 2 = ¬P ∨ C 2 , где P
                                 ′      ′
– пропозициональная буква, C1 и C2 – предложения (в частности, пустые или
содержащие только       одну букву или ее отрицание). Правило резолюций
                               ′     ′
формулируется так: С1 , С2 ├ C1 ∨ C 2 .
                                                                      ′    ′
     С1 , С2 называются резольвируемыми предложениями, а C1 ∨ C 2 –
резольвентой.
     Правило резолюций будем обозначать R .

     Теорема. Резольвента логически следует из резольвируемых предложений.
     Доказательство. В вышеприведенных обозначениях, нам нужно доказать, что
     (       ′(    ′    )
С1 → C 2 → C1 ∨ C 2 – тавтология (по теореме дедукции).
                                (    ′
                                      (   ′
     Предположим, что C1 → C 2 → C1 ∨ C 2 = 0 ⇔   )
                                                  ⎧ C1 = 1,
                              ⎧                   ⎪
 ⎧ C1 = 1,                    ⎪ C1 = 1,           ⎪ C2 = 1,
 ⎪                            ⎪                   ⎪ ′
⇔⎨
   C
 ⎪⎩ 2 →   (C1
             ′
               ∨ C 2)′
                       = 0,
                            ⇔ ⎨ C 2 = 1,
                              ⎪ ′        ′
                                              ⇔   ⎨ C = 0, ⇔
                                                  ⎪ 1
                              ⎪ C1 ∨ C 2 = 0,     ⎪ ′
                              ⎩                   ⎪ C2 = 0,
                                                  ⎩
 ⎧ C ′ ∨ P = 1,
 ⎪ 1               ⎧ P = 1,     ⎧ P = 1,
 ⎪ ′               ⎪            ⎪
 ⎪ C 2 ∨ ¬P = 1,   ⎪ ¬ P =  1,  ⎪ P = 0,
 ⎪                 ⎪            ⎪
⇔⎨               ⇔ ⎨ C ′ = 0, ⇔ ⎨ C ′ = 0,
 ⎪ C1′ = 0,        ⎪ 1          ⎪ 1
 ⎪                 ⎪ ′          ⎪ ′
 ⎪ ′               ⎪ C 2 = 0,   ⎪ C 2 = 0.
 ⎪⎩ C 2 = 0,       ⎩            ⎩
     Полученное противоречие доказывает утверждение теоремы.

     Правило резолюций применяется в опровержении методом резолюций –
алгоритме, устанавливающем выводимость Γ ├ A .


                                          25