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

UptoLike

ВУЗ: 

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

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

Рубрика: 

1) А ∨ А
2)
В ∨ А
3).
.А
4) А (1, 3)
5)
(3,4) Получена пустая формула. Теорема доказана.
15.5 Сведение формулы к множеству предложений
Любая формула ИП может быть преобразована в множество предложений
с помощью следующих замен (
≈> - знак замены).
1)
Элиминация импликации: А→В ≈> А ∨ В.
(Знак
→ устранен).
2)
Продвижение отрицания:  А ≈>А, (А ∨ В)
≈> А ∧ В, (А ∧ В) ≈> А ∨ В; ∀х А ≈>∃ х А, ∃ х А ≈> ∀х А. (Теперь
знаки
- только перед атомами.)
3)
Разделение связанных переменных: Q
1
х А
(…Q
2
хВ (…х…) …) ≈> Q
1
хА (…Q
2
yВ(…y…)…), где Q
1
, Q
2
– любые кванторы.
(Теперь нет случайно совпадающих связанных переменных.)
4)
Распространение кванторов: Q х А∨ B ≈> Q х
(А
∨ В), Q х А∧В≈> Q х ( А ∧ В). (Теперь, после замен 1-4, формула находится в
так называемой предваренной форме.)
5)
Элиминация кванторов существования:
∃ х
1
Q
2
х
2
… Q
n
х
n
А (х
1
, х
2
, …, х
n
) ≈>Q
2
х
2
… Q
n
х
n
А(а,х
2
,…, х
n
); ∀х
1
… ∀х
i-1
Q
i+1
х
i+1
… Q
n
х
n
А (х1,…,xi,…xn) ≈> ∀х
1
… ∀х
i-1
Q
i+1
х
i+1
… Q
n
х
n
А (х1,…,f
(х1, …, хi-1,… хn), где а – новая предметная константа, f – новый функтор, Q1,
Q2,…, Qn – любые кванторы. (После замен 1-5 формула содержит кванторы
только вида
∀.)
6)
Элиминация кванторов всеобщности: ∀х
А(х)
≈> А(х). (Теперь нет и кванторов ∀.)
7)
Приведение к КНФ:
А
∨ (В∧С) ≈>(А∨В) ∧ (А∨ С), (А∧В) ∨ С≈>(А∨ С) ∧ (В∨ С). (Имеем КНФ
после 1-7.)
8)
Элиминация конъюнкции: А∧В≈> А,В. (Те-
перь, после замен 1-8, имеем множество предложений.)
15.6 Обоснование метода резолюций
Теорема Если Г – множество предложений, полученных из формулы S, то
S является противоречием тогда и только тогда, когда множество Г невыпол-
нимо.
Напомним, невыполнимость множества формул означает, что не сущест-
вует интерпретации, в которой все формулы множества имеют значение «исти-
на». 
      1) А ∨ А
      2)  В ∨ А
      3)..А
      4) А (1, 3)
      5)    (3,4) Получена пустая формула. Теорема доказана.

       15.5 Сведение формулы к множеству предложений

        Любая формула ИП может быть преобразована в множество предложений
с помощью следующих замен (≈> - знак замены).
        1)                            Элиминация импликации: А→В ≈>  А ∨ В.
(Знак → устранен).
        2)                            Продвижение отрицания:  А ≈>А,  (А ∨ В)
≈> А ∧  В,  (А ∧ В) ≈> А ∨  В;  ∀х А ≈>∃ х  А,  ∃ х А ≈> ∀х  А. (Теперь
знаки  - только перед атомами.)
        3)                            Разделение связанных переменных: Q1 х А
(…Q2хВ (…х…) …) ≈> Q1 хА (…Q2 yВ(…y…)…), где Q1, Q2 – любые кванторы.
(Теперь нет случайно совпадающих связанных переменных.)
        4)                            Распространение кванторов: Q х А∨ B ≈> Q х
(А∨ В), Q х А∧В≈> Q х ( А ∧ В). (Теперь, после замен 1-4, формула находится в
так называемой предваренной форме.)
        5)                            Элиминация кванторов существования:
        ∃ х1 Q2 х2 … Qn хn А (х1, х2, …, хn) ≈>Q2 х2… Qn хn А(а,х2,…, хn); ∀х1… ∀х
i-1 Q i+1 х i+1… Qn хn А (х1,…,xi,…xn) ≈> ∀х1… ∀х i-1 Q i+1 х i+1… Qn хn А (х1,…,f
(х1, …, хi-1,… хn), где а – новая предметная константа, f – новый функтор, Q1,
Q2,…, Qn – любые кванторы. (После замен 1-5 формула содержит кванторы
только вида ∀.)
        6)                            Элиминация кванторов всеобщности: ∀х
А(х) ≈> А(х). (Теперь нет и кванторов ∀.)
        7)                            Приведение к КНФ:
        А∨ (В∧С) ≈>(А∨В) ∧ (А∨ С), (А∧В) ∨ С≈>(А∨ С) ∧ (В∨ С). (Имеем КНФ
после 1-7.)
        8)                            Элиминация конъюнкции: А∧В≈> А,В. (Те-
перь, после замен 1-8, имеем множество предложений.)

       15.6 Обоснование метода резолюций

      Теорема Если Г – множество предложений, полученных из формулы S, то
S является противоречием тогда и только тогда, когда множество Г невыпол-
нимо.
      Напомним, невыполнимость множества формул означает, что не сущест-
вует интерпретации, в которой все формулы множества имеют значение «исти-
на».

Страницы