Основные понятия и методы теории формальных систем. Волохович А.В. - 12 стр.

UptoLike

ВУЗ: 

НГТУ | Нижний Новгород

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

Рубрика: 

12
В, то город А' не торжествует. Требуется доказать, что город А'
торжествует тогда и только тогда, когда не торжествует город В'.
Запишем посылки и заключения на языке ИВ:
1) A
→ А';
2) В
→ В';
3) A
∨ B;
4) A
→
¬
В';
5) В
→
¬
А';
6) (А'
∨ В')&(
¬
В' ∨
¬
А').
Отметим, что
¬ [(А'
∨
В')&( ¬ В'
∨
¬ А')]= (А'&В')
∨
(
¬
В'
∨
¬
А')=
(А'
∨ ¬ В')& ( ¬ А' ∨ В').
Таким образом, требуется доказать противоречивость следующей
совокупности дизъюнктов:
1)
¬ A ∨ А'; 2)
¬
В ∨ В'; 3) A ∨ B; 4) ¬ A ∨ ¬ В';
5)
¬ В ∨ ¬ А'; 6) А' ∨
¬
В'; 7) В' ∨
¬
А'.
Конструируем резольвенты:
8) А'
∨
В (1,3);
9)
¬
В ∨ А' (2,6);
10) А' (8,9);
11 ) A
∨
¬
А' (3,5);
12 )
¬ A ∨ ¬ А' (4,7);
13)
¬ А' (11,12);
14) (10,13).
Решение закончено.
Теорема о полноте принципа резолюций.
Если конечная
совокупность дизъюнктов противоречива, то данный факт можно
доказать, основываясь на принципе резолюции, т. е. путем
последовательного конструирования резольвент, вплоть до
получения пустого дизъюнкта.
Верхняя оценка временной вычислительной сложности,
основанная на принципе резолюции алгоритма проверки
противоречивости КНФ, экспоненциальна, что связано с NР—
полнотой рассматриваемой проблемы.
При реализации данного
алгоритма осуществляется поиск
вывода пустого дизъюнкта. Некоторые направления поиска могут
оказаться тупиковыми, полученные при этом результаты в
найденном выводе пустого дизъюнкта не используются.
Так возникает вопрос о построении стратегий поиска,
обеспечивающих в случае противоречивости рассматриваемой
совокупности утверждений достаточно быстрый вывод пустого
дизъюнкта (по оценке "в среднем"). 
   В, то город А' не торжествует. Требуется доказать, что город А'
торжествует тогда и только тогда, когда не торжествует город В'.
   Запишем посылки и заключения на языке ИВ:
                  1) A → А';
                  2) В → В';
                  3) A ∨ B;
                  4) A → ¬ В';
                  5) В → ¬ А';
                  6) (А' ∨ В')&( ¬ В' ∨ ¬ А').
   Отметим, что
     ¬ [(А' ∨ В')&( ¬ В' ∨ ¬ А')]= (А'&В') ∨ ( ¬ В' ∨ ¬ А')=
    (А' ∨ ¬ В')& ( ¬ А' ∨ В').
   Таким образом, требуется доказать противоречивость следующей
совокупности дизъюнктов:
           1) ¬ A ∨ А';        2) ¬ В ∨ В';       3) A ∨ B; 4) ¬ A ∨ ¬ В';
           5) ¬ В ∨ ¬ А'; 6) А' ∨ ¬ В';           7) В' ∨ ¬ А'.
   Конструируем резольвенты:
                8) А' ∨ В                  (1,3);
                9) ¬ В ∨ А'                (2,6);
                10) А'                     (8,9);
                11 ) A ∨ ¬ А'              (3,5);
                12 ) ¬ A ∨ ¬ А'            (4,7);
                13) ¬ А'                   (11,12);
                14)                        (10,13).
   Решение закончено.
   Теорема о полноте принципа резолюций. Если конечная
совокупность дизъюнктов противоречива, то данный факт можно
доказать, основываясь на принципе резолюции, т. е.                      путем
последовательного         конструирования          резольвент,    вплоть   до
получения пустого дизъюнкта.
   Верхняя       оценка      временной        вычислительной       сложности,
основанная      на     принципе       резолюции         алгоритма    проверки
противоречивости КНФ, экспоненциальна, что связано с NР—
полнотой рассматриваемой проблемы.
   При реализации данного алгоритма осуществляется поиск
вывода пустого дизъюнкта. Некоторые направления поиска могут
оказаться тупиковыми, полученные при этом результаты в
найденном выводе пустого дизъюнкта не используются.
   Так возникает вопрос о построении стратегий поиска,
обеспечивающих в случае противоречивости рассматриваемой
совокупности утверждений достаточно быстрый вывод пустого
дизъюнкта (по оценке "в среднем").



12

Страницы