Математическая логика и теория алгоритмов. Стенюшкина В.А. - 41 стр.

UptoLike

ВУЗ: 

ОГУ | Оренбург

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

Рубрика: 

ложения (в том числе, пустые); тогда правило вывода
'2'1
2,1
C
C
CC
∨
Rназывается
правилом резолюции. Здесь С
1
, С
2
– резольвируемые предложения; С
1
′∨С
2
′ -
резольвента; R – название правила; Р,
Р – контрарные литералы.
Теорема Резольвента является логическим следствием резольвируемых
предложений.
Правило резолюции для ИП: пусть С
1
, С
2
– предложения в ИП, причем С
1
= Р
∨С
1
′, С
2
= Р ∨С
2
′, где P
1
, Р
2
– литералы, имеющие наиболее общий унифи
катор
σ; тогда правило вывода
σ
'2'1
2,1
C
C
CC
∨
R называется правилом резолюции.
Здесь резольвента (С
1
′∨С
2
′)σ получена из предложения (С
1
′∨С
2
′) применением
унификатора
σ.
Напомним, формулы А (…, х
i
, …), В (…, х
i
, …) называются унифицируе-
мыми, если существует набор подстановок
хi  хii =1 , в результате которых
будет выполняться равенство А (…, хi, …) = В (…, хi, …). Указанный набор
называется общим унификатором, наименьший набор из возможных называет-
ся наиболее общим унификатором (НОУ). В подстановках используются обоз-
начения хi – для переменных, хi – для формул, i =1 …n.
15.4 Метод резолюций
Пусть требуется установить выводимость
S
 G (15.2)
Тогда предварительно формулы множества S и формула
G независимо
преобразуются в множества предложений. (Множество предложений есть кон-
ъюнкция предложений). В полученном множестве всех предложений С отыски-
вается резольвируемые предложения, к ним применяется правило резолюции, и
резольвента добавляется в множество С. При повторных действиях возможны
случаи:
1) В результате очередного применения правила резолюции получено пу-
стое предложение. Это означает, что выводимость (15.2) установлена (теорема
доказана);
2)Среди текущего множества предложений С нет резольвируемых. Это
означает, что выводимости (2) нет ( теорема опровергнута);
3) Процесс продолжается, множество С пополняется, пустых предложе-
ний нет. Здесь не ясно.
Пример – Доказать теорему:

L
(((А→В) → А) →А)
Решение: Проведем тождественные преобразования:
(((А→В) → А) →
А) =
( ( ( А∨ В) ∨А) ∨А)= (((А ∧ В) ∨ А) ∨ А) = (А ∨ А) ∧ ( В ∨ А ) ∧ А.
Разбиваем на приложения и последовательно применяем правило резолюции: 
                                                           C1, C 2
ложения (в том числе, пустые); тогда правило вывода                Rназывается
                                                          C1'∨C 2'
правилом резолюции. Здесь С1, С2 – резольвируемые предложения; С1′∨С2′ -
резольвента; R – название правила; Р,  Р – контрарные литералы.
     Теорема Резольвента является логическим следствием резольвируемых
предложений.
     Правило резолюции для ИП: пусть С1, С2 – предложения в ИП, причем С1
= Р ∨С1′, С2 =  Р ∨С2′, где P1, Р2 – литералы, имеющие наиболее общий унифи

                                   C1, C 2
катор σ; тогда правило вывода               R называется правилом резолюции.
                                 C1'∨C 2' σ
Здесь резольвента (С1′∨С2′)σ получена из предложения (С1′∨С2′) применением
унификатора σ.
      Напомним, формулы А (…, хi, …), В (…, хi, …) называются унифицируе-
мыми, если существует набор подстановок  хi  хii =1 , в результате которых
будет выполняться равенство А (…, хi, …) = В (…, хi, …). Указанный набор
называется общим унификатором, наименьший набор из возможных называет-
ся наиболее общим унификатором (НОУ). В подстановках используются обоз-
начения хi – для переменных, хi – для формул, i =1 …n.

       15.4 Метод резолюций

      Пусть требуется установить выводимость

                                    S  G                                    (15.2)

      Тогда предварительно формулы множества S и формула G независимо
преобразуются в множества предложений. (Множество предложений есть кон-
ъюнкция предложений). В полученном множестве всех предложений С отыски-
вается резольвируемые предложения, к ним применяется правило резолюции, и
резольвента добавляется в множество С. При повторных действиях возможны
случаи:
      1) В результате очередного применения правила резолюции получено пу-
стое предложение. Это означает, что выводимость (15.2) установлена (теорема
доказана);
      2)Среди текущего множества предложений С нет резольвируемых. Это
означает, что выводимости (2) нет ( теорема опровергнута);
      3) Процесс продолжается, множество С пополняется, пустых предложе-
ний нет. Здесь не ясно.
      Пример – Доказать теорему:  L (((А→В) → А) →А)
      Решение: Проведем тождественные преобразования:  (((А→В) → А) →
А) =  ( ( ( А∨ В) ∨А) ∨А)= (((А ∧  В) ∨ А) ∨  А) = (А ∨ А) ∧ ( В ∨ А ) ∧  А.
Разбиваем на приложения и последовательно применяем правило резолюции:

Страницы