| Назад | Содержание |
Данная глава посвящена рассмотрению методов автоматизации поиска доказательства. В главе 20 при решении задач использовалась следующая схема. Пусть у нас имеются аксиомы или уже доказанные факты
F1, F 2, ..., Fm.
Нам требуется определить, следует ли утверждение Сиз утверждений F1, F 2, ..., Fm . Согласно теореме 2 о логическом следствии для решения этого вопроса нам достаточно определить, является ли формула
F1 & F2 & ... & Fm & ~ G.
противоречивой. Данную формулу можно преобразовать к равнозначной формуле, находящейся в КНФ, и в дальнейшем рассматривать множество дизъюнктов
S = {S1, S2, ..., Sn}.
По теореме о полноте метода резолюций для того, чтобы определить противоречивость (невыполнимость) множества S, достаточно найти опровержение в S. Правило резолюции позволяет извлекать новые данные из уже имеющихся, а теорема о резолюции гарантирует, что, если исходные дизъюнкты были истинными, то истинным будет и построенная по ним резольвента. Понятие вывода — формализованный аналог понятия доказательства.
Рассмотрим автоматические методы поиска доказательства. Теоретический материал иллюстрируется примерами, и предлагаются задания для создания сценариев, реализующих методы поиска решений.
Согласно теореме о полноте метода резолюций для того, чтобы доказать, что множество дизъюнктов противоречиво, достаточно построить опровержение в S.
При поиске опровержения строятся всевозможные резольвенты и добавляются к множеству дизъюнктов S. Построение резольвент продолжается до тех пор, пока не будет получен требуемый дизъюнкт П. Далее необходимо проследить в обратном порядке, как был получен дизъюнкт П, и восстановить вывод. При этом может оказаться, что порождено много лишних дизъюнктов, которые не нужны при построении вывода. Стратегия насыщения уровней состоит в следующем: формируются множества дизъюнктов .S°, S 1 , ..., S m , где
Когда резольвента построена, она добавляется к концу списка, сформированному на данный момент.
Пример доказательства противоречивости множества
Рассмотрим следующее множество дизъюнктов:
S = {- A v С, ~ В v С, ~ A v В v С, ~ С v D, A v D, ~ D}.
Требуется доказать, что оно противоречиво, и продемонстрировать на этом примере использование стратегии насыщения уровней.
S°: (1) ~ A v C
(2) ~ B v С
(3) ~ A v B v C
(4) ~ C v D
(5) A v D
(6) ~ D
S 1 : (7) ~ A v D из(1) и (4)
(8) C v D из (1) и (5)
(9) ~ A v С из (2) и (3)
(10) ~ В v D из (2) и (4)
(11) ~ A v B v D из (3) и (4)
(12) В v C v D из (3) и (5)
(13) ~ С из (4) и (6)
(14) А из (5) и (6)
(15) ~ A из (1) и (13)
(16) С из (1) и (14)
(17) ~ A v C v D из (2) и (11)
(18) С v D из (2) и (12)
(19) ~ В из (2) и (13)
(20) ~ A v B из(З) и (13)
(21) В v Сиз (3) и (14)
(22) D из (4) и (8)
(23) ~ A v D из (4) и (9)
(24) В v D из (4) и (12)
(25) D из (5) и (7)
(26) С v D из (5) и (9)
(27) ~ A из (6) и (7)
(28) С из (6) и (8)
(29). ~ В из (6) и (10)
(30) ~Av 5 из (6) и (11)
(31) В v Сиз (6) и (12)
S 3 : (32) ~ A v С из (2) и (21)
(33) С v D из (2) и (24)
(34) ~ A v С из (2) и (30)
(35) С из (2) и (31)
(36) ~ A v С из (3) и (19)
(37) ~ A v С из (3) и (29)
(38) D из (4) и (16)
(39) ~A v D из (4) и (17)
(40) D из (4) и (18)
(41) B v D из (4) и (21)
(42) D из (4) и (29)
(43) С v D из (5) и (17)
(44) B v D из (5) и (20)
(45) D из (5) и (23)
(46) D из (5) и (27)
(47) B v D из (5) и (30)
(48) П из (6) и (22)
Нетрудно видеть, что при поиске тождественно ложного дизъюнкта были порождены лишние дизъюнкты, не относящиеся к выводу. Многие дизъюнкты порождались неоднократно. На самом деле для того чтобы построить опровержение, требовалось породить дизъюнкты (8), (22), (48). На рис. 21.1 приведено дерево опровержения для
S,
построенное согласно стратегии насыщения уровней.
|
|
| Рис 21.1. Дерево опровержения согласно стратегии насыщения уровней |
Для следующего множества дизъюнктов
S = { C v M v D, ~ C v M v D, M v ~ D, ~ M v D, ~ D v С, ~ D}
найдите тождественно ложный дизъюнкт, воспользовавшись методом насыщения уровней.
Напишите сценарий, который по заданному множеству дизъюнктов находит дизъюнкт П, используя стратегию насыщения уровней. При этом требуется определить число порожденных дизъюнктов, длину построенного вывода и время, затраченное на поиск доказательства.
Для решения проблемы порождения избыточного числа дизъюнктов применяется стратегия вычеркивания.
Дизъюнкт С является поддизъюнктом дизъюнкта D, если верно С с D. Дизъюнкт D в этом случае называется наддизъюнктом для С.
Стратегия вычеркивания используется вместе со стратегией насыщения уровней следующим образом: сначала выписываются дизъюнкты из множества
(S° u... u Sn-1)
по порядку, затем вычисляются резольвенты путем сравнения каждого дизъюнкта C1e(S° u ... u Sn-1) с дизъюнктом С2еSn-1
Если резольвента является тавтологией или наддизъюнктом какого-либо дизъюнкта из списка уже построенных, она вычеркивается, в противном случае добавляется к порождаемому списку дизъюнктов.
Пример применения стратегии вычеркивания
Применим стратегию вычеркивания к поиску дизъюнкта П из множества дизъюнктов S, рассмотренного в предыдущем примере.
В методе насыщения уровней при построении резольвенты (9) получили дизъюнкт ~ A v С, который совпадает с дизъюнктом (1), построенную резольвенту в список не включаем. При построении резольвенты (17) был получен дизъюнкт ~ A v С v D, он также не включается в список, потому что является наддизъюнктом дизъюнкта ~ A v С. Приведем дальнейший список без комментариев.
S°: (1) ~ A v С
(2) ~ В v С
(3) ~ A v В v С
(4) ~ С v D
(5) AvD
(6) ~D
(7) ~ A v D из (l) и (4)
(8) С v D из (1) и (5)
(9) ~ В v D из (2) и (4)
(10) -AvBv £из(3)и(4)
(11) Bv С v Z) из (3) и (5)
(12) -Сиз (4) и (6)
(13) Л из (5) и (6)
(14) ~ А из (1) и (12)
(15) С из (1) и (13)
(16) ~ В из (2) и (12)
(17) D из (4) и (8)
(18) П из (6) и (17)
В этот список занесено 12 порожденных резольвент в отличие от 42 дизъюнктов из списка, полученного в результате использования стратегии насыщения уровней. Для построения опровержения требовалось породить дизъюнкты (8) и (17). Дерево вывода такое же, как и дерево, полученное по методу насыщения уровней (см. рис. 21.1), лишь нумерация дизъюнктов иная.
Для следующего множества дизъюнктов
S={Cv Mv D, ~ Cv Mv D, Mv~ D, ~ Mv D,~ Dv С, ~ D}
найдите тождественно ложный дизъюнкт, используя стратегию вычеркивания.
Напишите сценарий, который по заданному множеству дизъюнктов находит дизъюнкт П, используя стратегию вычеркивания. При этом требуется определить число порожденных дизъюнктов, длину построенного вывода и время, затраченное на поиск доказательства.
Линейная резолюция соответствует следующей схеме поиска доказательства. Мы выбрали некоторое утверждение из исходного множества, применили к нему и к другому утверждению правило резолюции, получили резольвенту. К полученной резольвенте и какому-либо другому дизъюнкту опять применили правило резолюции, получили следующее высказывание, и т. д. На каждом этапе построения доказательства одно из высказываний — это только что полученное в результате применения правила резолюции утверждение. Процесс повторяется до тех пор, пока не будет получен тождественно ложный дизъюнкт.
Рассмотрим множество дизъюнктов 5= {Si, $2 , ..., S n }. Возьмем дизъюнкт Q из S. Линейный вывод дизъюнкта С из множества дизъюнктов S — это вывод, изображенный с помощью схемы на рис. 21.2, в котором выполняются условия:
1. Для /=0, 1, ..., k~\ дизъюнкт С, +] есть резольвента дизъюнкта С/ (называемого центральным дизъюнктом) и Д (называемого боковым).
2.
Каждый
BI
либо принадлежит
S,
либо есть
Cj
для некоторого
j,
такого, что
j
< /.
|
| Рис 21.2. Схема построения линейного вывода |
Внимание трех девушек Екатерины, Елены и Евгении привлек проезжающий мимо автомобиль.
Оказалось, что каждая из трех девушек права только в одном из своих высказываний. Какой марки автомобиль, и в какой стране изготовлен?
Введем следующие обозначения:
Высказывания трех девушек с учетом того, что одно из них истинно, а одно ложно, записываются с помощью формул исчисления высказываний следующим образом:
Утверждение, что автомобиль изготовлен в одной из двух стран, соответствует формуле
Я & ~ G v ~ R&G.
И, наконец, утверждение, что проезжающий автомобиль принадлежит какой-либо из трех марок:
F&~M&~Av~F&M&~Av~F&~M&A.
Мы хотим определить, следует ли утверждение F & G (автомобиль марки Форд, изготовлен в Германии) из рассматриваемых пяти утверждений. Формулу
(R &~ Fv~ R& F) &(G&~ Л/v ~ G&M)&(G&~Av~ G&A)& (F&~M&~Av~F&M&~Av~F&~M&A)&~ (F& G)
преобразуем к КНФ и получим следующее множество дизъюнктов: S={Rv F, ~ Rv~ F, Gv М, ~ Gv~ M, GvA, ~ Gv~ A,Rv G, ~Rv~G,
~Fv~Mv~A, ~Fv~MvA, ~ Fv Mv ~ A, Fv~Mv~A, Fv Mv A, ~ Fv ~ G}.
Дизъюнкты множества S будем обозначать Si, S 2 , ..., 5 14 . В качестве верхнего дизъюнкта возьмем дизъюнкт S { . Построим линейный вывод, изображенный на рис. 21.3.
|
| Рис 21.3. Линейное опровержение для задачи об автомобилях |
1. Постройте линейный вывод для решения задачи об автомобилях, используя в качестве верхнего дизъюнкта дизъюнкт $ц.
2. Постройте опровержение согласно стратегии насыщения уровней для решения задачи об автомобилях.
3. Постройте опровержение согласно стратегии вычеркивания для решения задачи об автомобилях.
Напишите сценарий, который по заданному множеству дизъюнктов и выводу определяет, является ли этот вывод линейным.
Рассмотрим некоторые частные случаи линейной резолюции.
Каждый дизъюнкт исходного множества S назовем входным дизъюнктом.
Входная резолюция — это резолюция, в которой один из дизъюнктов входной дизъюнкт.
Входной вывод — линейный вывод, в котором каждое применение резолюции является входной резолюцией.
Входное опровержение —
входной вывод дизъюнкта П из
S.
Формируется экипаж для кругосветного путешествия. Каждый кандидат проходит тестирование. Окончательное слово остается за командиром экипажа. Три человека Семен, Максим и Дмитрий проходят тестирование. После беседы с ними командир высказал свое мнение помощнику необычным образом:
Никто не усомнился в том, что высказывания командира экипажа истинны. Дмитрий после собеседования на вопрос друга о том, отправляется ли он в кругосветное путешествие, ответил утвердительно. Прав ли Дмитрий?
Введем следующие обозначения:
Запишем формулами четыре высказывания командира экипажа и ответ Дмитрия:
Формулу, построенную согласно теореме 2 о логическом следствии:
(CvMvD)&(C&~D=*Af)&(D&Mv~D&~Af)&(D^C)&~D приведем к КНФ и получим интересующее нас множество дизъюнктов: 5={CvA/v Д ~ Cv Mv D, Mv~ D,~ Mv D, ~ D v С, ~ D}.
Считаем, что наши исходные дизъюнкты пронумерованы от
Si
до ^6- Построим входное опровержение в
S
(рис. 21.4).
|
| Рис 21.4. Линейное опровержение для задачи о формировании экипажа |
Обратите внимание на то, что в линейном выводе на рис. 21.4 все боковые дизъюнкты являются входными дизъюнктами, поэтому и опровержение — входное.
Постройте входное опровержение для задачи об автомобилях, используя дизъюнкт, отличный от
Si,
в качестве верхнего дизъюнкта.
Напишите сценарий, который по заданному множеству дизъюнктов и выводу определяет, является ли этот вывод входным.
Рассмотрим еще один частный случай линейной резолюции, так называемую единичную резолюцию.
Единичная резолюция — это резолюция, в которой, по крайней мере, один из дизъюнктов является единичным.
Единичный вывод — линейный вывод, в котором каждое применение резолюции является единичной резолюцией.
Единичное опровержение — единичный вывод дизъюнкта П из S.
Пример единичного опровержения
Построим единичное опровержение для задачи о формировании экипажа. Напомним, что рассматривается множество дизъюнктов
S= {Cv Mv Д ~ Cv Mv Д Mv~ D, ~ Л/v D, ~ Dv C, ~ D}.
На рис. 21.5 представлено единичное опровержение. Заметим, что это опровержение не является входным. При получении дизъюнкта П использовались дизъюнкты
S[i
и
Sj,
и дизъюнкт ^7 не является входным.
|
| Рис 21.5. Единичное опровержение для задачи о формировании экипажа |
Постройте единичное опровержение для задачи об автомобилях, используя дизъюнкт, отличный от
Si,
в качестве верхнего дизъюнкта.
Напишите сценарий, который по заданному множеству дизъюнктов и выводу определяет, является ли этот вывод единичным.
Эквивалентность входной и единичной резолюций
Теорема об эквивалентности входной и единичной резолюций
Для противоречивого множества дизъюнктов S единичное опровержение имеется тогда и только тогда, когда имеется входное.
Доказательство. Пусть А — множество пропозициональных переменных, входящих во множество дизъюнктов S (база S). Если А состоит из единственного элемента Q, то среди множества дизъюнктов S имеются единичные дизъюнкты Q и ~ Q. Резольвентой дизъюнктов Q и ~ Q является дизъюнкт П. Вывод дизъюнкта П из 5 является как входным, так и единичным. Следовательно, для этого случая теорема верна.
Предположим, что теорема верна для случая, когда множество А состоит из / элементов, где 1 < i < п.
Пусть имеется единичное опровержение в S. Тогда множество дизъюнктов S должно содержать хотя бы один единичный дизъюнкт L, где L — литерал. Множество дизъюнктов S * получаем из S исключением дизъюнктов, содержащих L, и вычеркиванием литерала ~ L из остальных дизъюнктов. Поскольку множество S противоречиво, то противоречивым будет и множество S", т. к. S* мы получили по правилу единичного дизъюнкта. Раз имеется единичное опровержение в S, то должно существовать единичное опровержение в S*.
База множества дизъюнктов S* содержит п или менее элементов. По индукционному предположению имеется £ "-входное опровержение Z\. Пусть Z — вывод, получающийся из Z\ возвращением литерала ~ L в те дизъюнкты, из которых он был вычеркнут.
Пусть литерал
Т' —
дизъюнкт, получившийся в корне дерева для вывода
Z.
Очевидно, что Z является ^-входным выводом дизъюнкта
Т
из
S.
Дизъюнкт
Т—
это либо П, либо ~
L.
Если
Тесть
П, то мы построили входное опровержение в
S.
Если же
Т
есть ~
L,
то строим резольвенту
Т
с дизъюнктом
L,
который является входным дизъюнктом. Таким образом, и в этом случае мы построили входное опровержение.
Для задачи о формировании экипажа на рис. 21.6 приведено единичное опровержение. Рассматриваемое множество дизъюнктов
S=
{CvMv
D, ~
CvA/v
D, Mv~ D,~
Mv
D,
~Z)v
С, ~ D}
содержит единичный дизъюнкт ~
D.
|
| Рис 21.6. Единичное опровержение для задачи о формировании экипажа после сокращения дизъюнктов |
Построим множество S" исключением из S всех дизъюнктов, содержащих литерал ~ D, и вычеркиванием из оставшихся дизъюнктов литерала D. Получим
S* = {CvM, ~ CvM, ~ М].
На рис. 21.6 приведем единичное опровержение
Z\
в
S*.
Это опровержение входное. Вывод Z получим, возвращая литерал
D
в те дизъюнкты, из которых он был вычеркнут. Получим вывод
Z,
изображенный на рис. 21.7.
|
| Рис 21.7. Входной вывод сокращенного дизъюнкта |
Вывод Z является 5-входным выводом дизъюнкта
D
из
S.
На рис. 21.8 построено ^-входное опровержение.
|
| Рис 21.8. Входное опровержение для задачи о формировании экипажа |
Предположим, что имеется входное опровержение в S. Множество S должно содержать, по крайней мере, один единичный дизъюнкт L. Такой литерал необходим при получении дизъюнкта П, один из исходных дизъюнктов должен быть входным. Обозначим через N множество дизъюнктов, в которых содержатся литералы L или ~ L, через Res(7, Q — резольвенту дизъюнктов Уи С. Построим множество
S* = Ju {Res(£, QI CeS} - N.
Так как существует ^-входное опровержение, то должно существовать
S*-
входное опровержение. Но множество
S*
содержит
п
или менее пропозициональных переменных. По индукционному предположению можно построить единичное опровержение в
S*.
Каждый дизъюнкт из
S*
является либо дизъюнктом из
S,
либо резольвентой, полученной применением единичной резолюции к дизъюнкту
L
и некоторому дизъюнкту из
S.
Поэтому можно построить единичное опровержение в
S.
Теорема доказана.
Пример построения входного опровержения
Рассматриваемое множество дизъюнктов таково:
S= {Cv Л/v D, ~ Cv Л/v D, Л/v ~ D, ~ Л/v D, ~ D v С, ~ D}.
На рис. 21.3 построено входное опровержение в S. Множество S содержит, по крайней мере, один единичный дизъюнкт. Обратите внимание на построение резольвенты по дизъюнктам 5 10 и S^. В нашем случае это дизъюнкт ~ D. Множество N совпадает с S, т. к. каждый дизъюнкт из £ содержит либо D, либо ~ D.
Есть множество
{Res(I, C)\CeS} = {Cv Л/, ~ СУ М, ~ Л/}. Построим множество
Si = 5и {Res(Z, Ol CeS} - N= {Cv A/, ~ Cv Л/, ~ Л/}.
На рис. 21.9 изображено ^-входное опровержение. Заметим, что оно одновременно является и единичным опровержением.
|
| Рис 21.9. Входное опровержение для множества S-i |
На рис. 21.10 показано, как по
S\
-входному опровержению можно построить единичное опровержение в
S.
|
| Рис 21.10. Единичное опровержение, построенное по входному |
Определите, можно ли построить единичное опровержение для задачи о формировании экипажа.
1. Напишите сценарий, который по заданному входному ^-опровержению строит единичное ^-опровержение.
2. Напишите сценарий, который по заданному единичному 5-опровержению строит входное ^-опровержение.
Свойства входной и единичной резолюций
Единичную и входную резолюцию легче реализовать, чем другие стратегии поиска доказательства, но у входной и единичной резолюций есть один существенный недостаток: обе стратегии не являются полными.
Задача о кандидатах в министры
В одной стране проживают рыцари, которые говорят только правду, лжецы, которые всегда лгут, и так называемые нормальные люди. Нормальный человек может говорить как правду, так и ложь. Три различные партии (обозначим их Е, F и G) выдвигают на пост министра трех кандидатов: А, В и С соответственно. Каждый из кандидатов, выступая от имени своей партии, предложил программу развития экономики. После встречи с президентом во время пресс-конференции на вопрос журналиста: "Программа какой партии получила одобрение президента?" каждый из кандидатов ответил:
В этот же день во время прямого телеэфира телеведущая задала кандидатам тот же самый вопрос: "Программа какой партии получила одобрение президента?" и получила уже другие ответы:
Известно, что один из кандидатов — рыцарь, один — лжец, и один — нормальный человек, который в одном случае сказал правду, а в другом ложь. Программа какой партии получила одобрение президента?
Для решения задачи введем обозначения. Обозначим через Е (соответственно F и G) утверждение, что получила одобрение президента программа, предложенная партией (соответственно F к G). Тогда высказывания кандидатов журналисту и ведущему имеют следующий вид:
Так как известно, что один из кандидатов — рыцарь, один — лжец и один — нормальный человек, то возможны следующие шесть вариантов, которые представлены в табл. 21.1.
Таблица 21.1. Варианты кандидатов
|
№
|
Кандидат А
|
Кандидат В
|
Кандидат С
|
|
1
|
рыцарь
|
лжец
|
нормальный человек
|
|
2
|
рыцарь
|
нормальный человек
|
лжец
|
|
3
|
лжец
|
рыцарь
|
нормальный человек
|
|
4
|
лжец
|
нормальный человек
|
рыцарь
|
|
5
|
нормальный человек
|
рыцарь
|
лжец
|
|
6
|
нормальный человек
|
лжец
|
рыцарь
|
Учитывая, что высказывания рыцаря истинны, лжеца ложны, а из двух высказываний нормального человека одно ложно, а одно истинно, получаем следующую формулу, описывающую условие задачи и соответствующую рассмотренным шести вариантам:
~ Е&~ F& Е&~ G& (~G&~EvG&.E)v
~E&~F&(~E&~GvE&G)&G&~Ev
E&F&~E&G&(~G&~EvG&E)v
Е & F& (~ Е & ~ G v Е & G) & ~ G & Е v
(~E&FvE&~F)&~E&G&G&~Ev
(~E&FvE&~F)&E&~G&~G&E.
Эту формулу можно упростить, выполняя эквивалентную замену формул вида
/ &П <-> П и /v П <н>/ Получим следующую формулу:
~E&~F&(~E&~GvE&G)&G&~Ev
E&F&(~E&~GvE&G)&~G&Ev
(~ E&FVE&~ F)&~ E&G&G&-EV
(~E&FvE&~F)&E&~G&~G&E.
Приведем последнюю формулу к КНФ. Для этого вычислим ее значения во всех интерпретациях и результаты представим в табл. 21.2.
Таблица 21.2. Таблица истинности для формул задачи
|
Е
|
F
|
G
|
Значение формулы
|
|
и
|
и
|
и
|
л
|
|
и
|
и
|
л
|
л
|
|
и
|
л
|
и
|
л
|
|
и
|
л
|
л
|
и
|
|
л
|
и
|
и
|
и
|
|
л
|
и
|
л
|
л
|
|
л
|
л
|
и
|
л
|
|
л
|
л
|
л
|
л
|
Заметим, что одобрение президента получила только одна программа, поэтому рассмотрим формулу
E&~F&~Gv~E&F&~Gv~E&~F&G. Построим для этой формулы КНФ, а результаты представим в табл. 21.3.
Таблица 21.3. Таблица истинности
|
Е
|
F
|
G
|
Значение формулы
|
|
и |
и
|
и
|
л
|
|
и
|
и
|
л
|
л
|
|
и
|
л
|
и
|
л
|
|
и
|
л
|
л
|
и
|
|
л
|
и
|
и
|
л
|
|
л
|
и
|
л
|
и
|
|
л
|
л
|
и
|
и
|
|
л
|
л
|
л
|
л
|
Предположим, что мы хотим показать, что одобрение получила программа партии Е. После построения КНФ по табл. 21.2 и 21.3, и добавления предполагаемого следствия, интересующее нас множество дизъюнктов будет следующим:
S = {~ Е v ~ F v ~ G, ~ Е v ~ F v G, ~ Е v F v ~ G, E v ~ Fv ~ G, Ev~FvG,EvFv~G, Ev Fv G, ~ E}.
Сократим множество S по правилу единичного дизъюнкта, получим множество S\.
{- Fv ~ G, ~ Fv G, Fv ~ (7, Fv G}.
Это множество противоречиво, если противоречиво исходное множество S. Линейное опровержение с верхним дизъюнктом ~ Fv ~ G изображено на рис. 21.11. Заметим, что линейный вывод на рис. 21.11 не является входным, т. к. боковой дизъюнкт ~ F не содержится в S.
|
| Рис 21.11. Линейное опровержение для задачи о кандидатах в министры |
Для множества дизъюнктов
{- Fv ~ G, ~ Fv G, Fv ~ G, Fv G)
нельзя построить единичного опровержения, а, следовательно, по теореме об эквивалентности входной и единичной резолюции нельзя построить и входное опровержение. Таким образом, методы входной и единичной резолюций не являются полными.
Теорема о полноте метода линейной резолюций
Пусть С— дизъюнкт, принадлежащий противоречивому множеству дизъюнктов S, если S - {С] выполнимо, то существует линейное опровержение из S с верхним дизъюнктом С,
Доказательство. Будем доказывать теорему индукцией по числу элементов базы А множества дизъюнктов S. Если А состоит из одного элемента Q, то во множестве S должен быть и элемент ~ Q. Их резольвентой является дизъюнкт П. Так как S- (Q выполнимо, то либо литерал Q, либо литерал ~ Q должен совпадать с литералом С. Теорема для этого случая доказана.
Предположим, что теорема верна для случая, когда А состоит из / элементов при 1 < /' < п. Рассмотрим множество А, состоящее из я+1 элемента.
Пусть С— единичный дизъюнкт, совпадающий с литералом L. Пусть S имеет вид:
S= {L, А\ v L,A 2 v L, ...,A m v L, BI v ~ L, ..., B k v ~ L, R { , ..., R q }.
Дизъюнкты Л ь ..., Rq не содержат ни литерала L, ни литерала ~ L. Построим множество S[ удалением из S дизъюнктов, содержащих L, и вычеркиванием литерала ~ L из остальных дизъюнктов. Множество S\ имеет вид
^1 = (В\, •••> Дь R\, •••, Rq}-
Так как множество S — противоречиво, то и множество дизъюнктов S\ — противоречиво. Пусть Jj — противоречивое подмножество S\ такое, что каждое собственное подмножество Т\ выполнимо. Для того чтобы получить такое подмножество, надо перебрать всевозможные подмножества множества S\.
Множество Т\ должно содержать дизъюнкт Е\, который был получен из некоторого дизъюнкта вида B t v ~ L, принадлежащего множеству дизъюнктов S, до вычеркивания литерала ~ L. Если бы это было не так, то все дизъюнкты множества Т\ принадлежали бы множеству дизъюнктов {Ль ..., R q ]. По условию теоремы множество дизъюнктов
.S- {Q = {А { v L, A 2 v L,..., A m v L, В^ ~ L, ..., B k v ~ L, Л ь ..., R q }
выполнимо. Следовательно, существует интерпретация, в которой выполнимо множество дизъюнктов {Л ь ..., Л ? }. Но тогда и множество Т\ являлось бы выполнимым, а это противоречит построению множества Т\. Итак, во множестве Т\ есть дизъюнкт Е\, совпадающий с В.
Множество дизъюнктов Т\ - {Е\} выполнимо, т. к. Т\ строилось таким образом, чтобы каждое его собственное подмножество было выполнимым. Множество Т\ содержит п или менее элементов, по индукционному предположению существует линейное опровержение D\ из Т\ с верхним дизъюнктом Е\. Преобразуем вывод D\. возвратим литерал ~ L в те дизъюнкты, из которых он был вычеркнут, за исключением верхнего дизъюнкта Е\. Дизъюнкт Е\ получим в результате выполнения резолюции дизъюнкта L с дизъюнктом EI v ~ L. Таким образом, построили вывод D либо дизъюнкта П, либо дизъюнкта ~ L в S. Если построили вывод дизъюнкта ~ L, то строим резольвенту дизъюнктов ~ L и L, получаем линейный вывод дизъюнкта П из S. Теорема в этом случае доказана.
Предположим, что С — не единичный дизъюнкт. Пусть L — первый (самый левый) литерал в С, т. е. С= L v С\, где С\ — непустой дизъюнкт. Пусть S\ — множество, получаемое из S удалением дизъюнктов, содержащих дизъюнкт ~ L, и вычеркиванием литерала L из всех оставшихся дизъюнктов. Если множество S имеет вид:
S={LvC l ,Lv С 2 , ..., L v C m , ~ L v В 1г ..., ~ L v B k , Л ь ..., R q }. то множество S\ будет выглядеть так:
S l = {C l ,C 2 , ..., C m , Л Ь ...,Л ? }.
Так как множество S — противоречиво, то и множество дизъюнктов S\ будет противоречивым. Рассмотрим множество
Si-{C 1 } = {C 2 ,...,C m ,R l ,. ... Л,}.
Докажем, что множество S\ - {Q} выполнимо. Пусть /— интерпретация, в которой выполнимо множество дизъюнктов
'S- {Q = {L v С 2 , ..., L v C m , ~ L v BI, ..., ~ L v B k , Л ь ..., R q }-
Такая интерпретация существует по условию теоремы. Так как S невыполнимо, то дизъюнкт С должен быть ложен в /. Поэтому литерал L ложен в интерпретации J. В интерпретации /истинны дизъюнкты С\, С 2 , ..., C m , R\, ..., R q следовательно, множество S\- {С\} истинно в J, т. е. S\ - {C\} выполнимо.
Поскольку множество элементов базы S\ содержит п или менее символов, то по индукционному предположению существует линейный вывод D\ дизъюнкта из iSi с верхним дизъюнктом С\. Возвращая литерал L во все дизъюнкты, из которых он ранее был вычеркнут, мы получим линейный вывод D\ дизъюнкта L из S с верхним дизъюнктом С.
Рассмотрим множество
Щ и (S - {Q) = {L, L v Ci,LvC 2 ,...,Lv C m ,~ Lv B } , ..., ~LvB k ,Ri, ..., R q }.
Докажем, что оно противоречиво. Предположим, что это не так, т. е. существует интерпретация /, в которой
{L}
и
(S
- (Q) выполнимо. В этой интерпретации значение литерала
L
истинно, но тогда в интерпретации / множество
S
истинно, что противоречит условию теоремы. Итак, множество дизъюнктов
Щ
u
(S - {€})
противоречиво. Множество
S - {Q
выполнимо,
L
— единичный дизъюнкт. Ранее доказали, что существует линейное опровержение Z>2 с верхним дизъюнктом
L
из множества
Щ
u
(S- {С}).
Объединяя выводы
DI
и Z>2, получим линейное опровержение из
S
с верхним дизъюнктом
С.
Теорема доказана.
Задача о поиске острова сокровищ
Предположим, что некоторый искатель приключений хочет добраться до острова сокровищ. Путешественнику предложили три карты: X, Y и Z. Только одна из карт правильная и указывает путь к острову сокровищ. В комнате, где лежали карты, находились пятеро колдунов: А, В, С, D и Е. Каждый колдун был либо рыцарем, либо лжецом и каждый дал путешественнику совет:
Какая же из карт правильная?
Докажем, что Y— правильная карта. Будем обозначать через А утверждение "А — рыцарь" (аналогично для В, С, D и Е). Обозначим через X утверждение "X' — правильная карта" (аналогично для Y и Z). Запишем сначала советы колдунов и предполагаемое следствие формулами исчисления высказываний:
Построим КНФ для формулы вида
/1 & F 2 & FI & /4 & F 5 & ~ G.
После преобразований получено множество дизъюнктов S, приведенное в табл. 21.4.
Таблица 21.4. Исходное множество дизъюнктов
|
S,:EvCvD
|
5ц: ~ Cv/4 v6
|
|
S
2
: Е
v ~
С
v D
|
S
12
: С v ~ Л v 6
|
|
83'.
~
Е
v ~
Cv D
|
S
13
: Cv,4v~ 6
|
|
S
4
: Е v ~
С
v ~ D
|
Si4
:
С V ~ /4 V ~ В
|
|
S
5
: ~ Ev Cv ~D
|
S
15
: Dv>AvS
|
|
S
6
: E v
С
v ~ D
|
S
16
: ~ D v ~ Л v
В
|
|
S
7
: ~
A v X
|
S
17
: D v /A v ~ 6
|
|
S
8
:
A
v ~
X
|
S
18
: D v ~
A
v ~ 6
|
|
S
9
: ~
В
v У
|
Si
9
: ~ У
|
|
S
10
: 6 v ~ V
|
|
В табл. 21.4 выделим те дизъюнкты и литералы, которые будем исключать из множества после преобразования по правилу единичного дизъюнкта (дизъюнкт ~ Y). Получаем множество дизъюнктов, размещенных в табл. 21.5.
Таблица 21.5. Дизъюнкты после сокращения по ~Y
|
Ev Cv D
|
~ Cv
A
v
В
|
|
Ev~ Cv D
|
Cv~ Av В
|
|
~
E
v ~
С
v
D
|
Cv A
v~
В
|
|
Ev
Cv D
|
~
Cv
A v В
|
|
Ev ~ Cv 'vD
|
С v ~
A
v ~ Б
|
|
~ E
vCv ~D
|
Dv Av В
|
|
E
v С v ~ D
|
~ D v ~Л v
В
|
|
~X»vX
|
DvAv ~B
|
|
>Av~X
|
D v ~ A
v ~6
|
|
~S
|
|
После преобразования по правилу единичного дизъюнкта (дизъюнкт ~ В) получим множество дизъюнктов, размещенных в табл. 21.6.
Таблица 21.6. Дизъюнкты после сокращения по ~Б
|
S
r
:
E
v С v
D
|
S
7
:~AvX
|
|
S
2
: E
v ~ С v D
|
S
8
: Л v ~ X,
|
|
83.' ~ £ v ~ С v D
|
S
9
: Cv ~A
|
|
S
4
: E v ~ С v ~ D
|
S
10
: ~CvA
|
|
S
5
:~EvCv ~D
|
S
n
;~Dv ~Л
|
|
S
6
: E v С v ~ D
|
S
12
: D\r A
|
Линейное опровержение, построенное из последнего множества дизъюнктов, может быть таким:
< 5i: E v С v D, S 2 : E v ~ С v D> -* S {3 : E v D;
< S n : E v D, S 4 : E v ~ Cv ~ D> ^> S^. Ev C;
<S H : Ev C, S 5 :~ Ev Cv- D> ^ S i5 : Cv ~D;
< Si 5 : С v ~D, S 6 : E v С v ~ D> -» 5i 6 : ^ v ~D\
< S 16 : E v ~D, S [3 : E v D > -> S {7 : E;
< S {7 : E, 5 3 : ~ Ev ~ Cv D> -» S 18 : ~ С v D;
< Si S :~Cv D, S 9 : С v ~ A > -* 5 l9 : ~ ^v Д
< 5, 9 : ~ /4v Д 5 12 : /) v /1 > -> ^20: A
< ^20: A ^5: ~ -£v Cv ~ Z» -» ^r ~ ^v C;
< 521: ~ E v C, S 17 : E > -^ ^22: C;
< 622: C, .SIQ: ~ Cv A> -> S 2 3- A;
< $23: A, 5 n : ~ О v ~ A > -> ^ 24 : ~Д
< ^4: ~Д £ 2 о: £» -> П.
1. Определите, какие дизъюнкты множества дизъюнктов SB задаче об автомобилях могут быть использованы в качестве верхних дизъюнктов в линейном выводе.
2. Определите, какие дизъюнкты множества дизъюнктов
S
в задаче о кандидатах в министры могут быть использованы в качестве верхних дизъюнктов в линейном выводе.
3. Напишите сценарий, который по заданному множеству дизъюнктов S определяет те дизъюнкты, которые могут быть использованы в качестве верхних дизъюнктов в линейном выводе.
4. Напишите сценарий, который по заданному множеству дизъюнктов
S
и некоторому дизъюнкту из
S
определяет, можно ли построить линейный вывод с этим верхним дизъюнктом, и строит вывод, если это возможно.
При построении опровержения можно придерживаться определенной стратегии. Каждая из стратегий имеет свои достоинства и недостатки. Один из основных вопросов стратегии состоит в том, полна ли она, т. е. всегда ли можно построить опровержение из противоречивого множества дизъюнктов согласно выбранной стратегии.
При поиске доказательства порождается большое число дизъюнктов, которые в дальнейшем могут не использоваться. Для того чтобы сократить множество порождаемых дизъюнктов, исходное множество S разбивается на два множества Z] и Z2. При построении вывода не разрешается строить резольвенту по двум дизъюнктам, принадлежащим одному множеству. При разбиении множества S на два множества Z.i и Е2 будет использована произвольная интерпретация /.
Пусть
S—
противоречивое множество дизъюнктов, /— произвольная интерпретация. Во множество Zi включим все дизъюнкты из
S,
истинные в интерпретации /, а во множество Z2 —
все
дизъюнкты, ложные в /.
Пример разбиения множества дизъюнктов
При решении задачи о кандидатах в министры было построено следующее множество дизъюнктов:
S = {~ Е v ~ F v ~ G, ~ Е v ~ Fv G, ~ E v Fv ~ G, Ev ~ F v ~ G,
Ev ~ Fv G, Ev Fv ~ G, Ev Fv G, ~ £}.
Рассмотрим интерпретацию I = (Е,~ F, G}. В этом случае множества Zi и Zj будут следующими:
Интерпретация I = {~ E, F, G} разобьет исходное множество S на следующие два множества
Лемма. Пусть S— противоречивое множество дизъюнктов, /— произвольная интерпретация. Во множество Zj включим все дизъюнкты из S, истинные в интерпретации /, а во множество S2 — все дизъюнкты, ложные в /. Доказать, что Zi и ЕЗ ~ непустые множества.
Предположим сначала, что множество Е 2 пусто, т. е. множество S совпадает с множеством Zj. Мы нашли интерпретацию, в которой £ выполнимо, а мы рассматриваем противоречивое множество S. Следовательно, множество £2 не может быть пустым.
Предположим теперь, что множество Zj пусто, т. е. мы нашли интерпретацию, в которой все дизъюнкты из S ложны. Но тогда мы должны признать, что в дизъюнктах ^ дляу= 1, ..., п нет ни одной контрарной пары. Если бы это было не так, то во множестве дизъюнктов S была бы пара дизъюнктов $ц и SQ вида:
Зц <-> Ац v Lv Бц и Sft <-> Af2 v ~ L v Bj2.
В выбранной интерпретации /значения дизъюнктов 3ц и S^ отличались бы: одно из них должно быть истинным, другое ложным. Мы же предположили, что все дизъюнкты ложны. Следовательно, во множестве S нет контрарных пар. По интерпретации / = {т\, mi, ...', т^} построим интерпретацию /* = = {~ mi, ~ т 2 , ..., ~ /я*}. В интерпретации /* все дизъюнкты из S истинны; как и в первом случае, мы нашли интерпретацию, в которой S выполнимо, а этого не может быть, т. к. S — противоречиво. Следовательно, предположение, что Zi пусто, неверно. Лемма доказана.
С целью дальнейшего сокращения числа порождаемых дизъюнктов на множестве элементов базы задается отношение порядка. При построении резольвенты по дизъюнктам
Si
и
$2
удаляемый литерал
в Si —
наибольший в этом дизъюнкте.
Рассмотрим следующее множество дизъюнктов:
S= {~ Ev ~ Fv ~ G, ~ E\r ~ Fv G, ~ Ev Fv ~ G, Ev ~ Fv ~ G,
Е\/ ~ Fv G, Ev Fv ~ G, Ev Fv G, ~ Е}.
Если в качестве одного из дизъюнктов взять дизъюнкт S\, то можно построить следующие резольвенты:
Если задан порадок
Е > F>G,
то допустимой является первая резольвента, если порядок
F>
E>G,
то следует строить вторую резольвенту, и, наконец, если порядок определен
G > Е > F,
то должна быть построена третья резольвента.
Определение семантического конфликта
Рассмотрим множество дизъюнктов S, выберем некоторую интерпретацию /, на элементах базы S зададим порядок Р.
Конечное множество дизъюнктов вида (Ei, Е 2 „ E q , N}, где q > 1 называется семантическим конфликтом, если Е\, Е 2 , ..., E q и 7V удовлетворяют следующим условиям:
1. Дизъюнкты EI, Е 2 , ..., Eg ложны в интерпретации /.
2. Пусть RI = N, для каждого /= 1, ..., q имеется резольвента R]+\ дизъюнктов Ri и Ei (рис. 21.12).
3. Тот литерал в Е/, по которому строится резольвента, наибольший в Е/.
4. Дизъюнкт Rg+i ложен в интерпретации /.
Дизъюнкт Rg+i называется семантической или ^/-резольвентой, обозначать семантическую резольвенту будем следующим образом:
{Е { , Е ъ ..., E q , N] -> Rg+i.-
Рис. 21.12.
Схема построения семантической
резольвенты
Пример построения семантического конфликта
Рассмотрим множество дизъюнктов, построенное при решении задачи об автомобилях:
S={Rv F, ~ Rv~ F, Gv M, ~ Gv~ M, Gv A,~ Gv~ A,Rv G,
~ R-v ~ G, ~ Fv ~ Mv ~ A, ~ Fv ~ Mv A, ~ Fv Mv ~ A, Fv~Mv~A, FvMvA,~Fv~ G}.
Выберем следующую интерпретацию / = {R, F, G, ~ M, А}, на множестве элементов базы зададим порядок R> G> F> M> A.
Множество дизъюнктов (~ Fv ~ G, ~ Rv ~ F, Rv G} является семантическим конфликтом (рис 21.13). Дизъюнкт ~ /'является построенной по семантическому конфликту резольвентой
{- F\/ ~ G, ~ R v ~ F, R v G] -> ~ F.
Рис. 21.13. Построение семантического конфликта
Пусть / — интерпретация некоторого множества дизъюнктов S; P — порядок на элементах базы. Вывод из множества S называется семантическим или Pi-выводом, если каждый дизъюнкт вывода либо принадлежит S, либо является PI-резольвентой.
Pi-вывод дизъюнкта D называется
Pi-опровержением.
В Олимпиаде по математике участвовали три ученика (обозначим их А, В, С). Когда А подошел к учителю узнать об итогах, тот ему сказал: "Если победитель ты, а не Д то и С также победитель". Второй ученик получил следующий ответ: "Если С— победитель, то либо ты, либо А также победители". Встретив ученика С, учитель произнес: "Если А — победитель, то ты точно не победитель". Чтобы утешить своих учеников, преподаватель на прощание сказал: "Среди вас точно есть победитель". Ученики предположили, что преподаватель не шутит и все его высказывания истинны. Является ли ученик В победителем?
Обозначим через А утверждение "А — победитель Олимпиады" (соответственно для В и С). Утверждения учителя и предполагаемое следствие запишутся формулами:
Построим множество дизъюнктов S:
S={~AvBvC,AvBv~C,~Av~C,AvBvC,~B}.
Выберем интерпретацию / = {- А, В, ~ С] и определим порядок А > В > С. Интерпретация /разбивает исходное множество S на два:
Zi = {~ A v В v С, A v В v ~ С, ~ A v ~ С, A v В v С,}; Z 2 = i~ В}.
Приведем семантическое опровержение, указывая семантический конфликт и построенную по нему PI-резольвенту:
{~ В, A v В v Q -> A v С;
{Л v С, ~ Д ~ Л v В v Q -> С;
(С, ~ 5, Л v Bv ~ Q-+A;
{А, С, ~ A v ~ Q -» П.
Н рис 21.14 изображено дерево, соответствующее построенному PI - опровержению
Рис. 21.14. Семантическое опровержение для задачи об Олимпиаде
Теорема о полноте метода семантической резолюции
Пусть S— противоречивое множество дизъюнктов; 7— произвольная интерпретация множества S; P —упорядочение на множестве элементов базы А. Существует Pi-опровержение в S.
Доказательство. Пусть множество А состоит лишь из одного элемента Q. Так как множество дизъюнктов S противоречиво, то среди дизъюнктов S есть дизъюнкты Q и ~ Q. Поскольку один из дизъюнктов Q или ~ Q ложен в /, то можно построить PI-резольвенту дизъюнкта П. Для этого случая теорема доказана.
Допустим, что теорема верна в тех случаях, когда множество А состоит из / элементов, где 1 < / < и. Рассмотрим случай, когда множество А состоит из п+ 1 элемента. При доказательстве исследуем два варианта.
Предположим, что множество
S
содержит единичный дизъюнкт
L,
ложный в интерпретации /. Построим множество
S*
следующим образом: исключим из множества
S
все дизъюнкты, содержащие литерал
L, a
из оставшихся дизъюнктов вычеркнем литерал ~
L.
Так как
S
противоречиво, то противоречивым будет и построенное множество
S*.
Множество элементов базы для
S*
содержит менее
п+\
элемента, поэтому по индукционному предположению существует Pi-опровержение
D*
в
S*.
При построении Pi-опровержения в S будем исследовать каждый дизъюнкт Pi-вывода D* в S*. Предположим, что дизъюнкт DJ в D* получен из семантического конфликта вида:
<E* l ,E 2 ,...,E' g ,L,N>.
Если дизъюнкт N* был получен из дизъюнкта TV вычеркиванием литерала ~ L, то будем рассматривать семантический конфликт
<El t E' 2i ...,E' q ,L,N>,
который порождает тот же дизъюнкт. Если дизъюнкт
Е*
получен из дизъюнкта
E
t
вычеркиванием литерала ~
L,
то будем рассматривать его как Pi-резольвенту семантического конфликта
<L, Е/>.
После описанных преобразований мы получим Pi-вывод дизъюнкта
DJ
из множества
S.
Выполняя преобразования над каждым дизъюнктом Pi-опровержения
D*
в
S*,
построим Pi-опровержение
D
в
S.
Пример построения семантического опровержения: вариант 1
Рассмотрим следующее множество дизъюнктов:
S = {~ A v В, ~ В v С v ~ A, D v A, D v ~ С, ~ D v A~ D}.
База множества S состоит из элементов {А, В, С, D}. Зададим порядок RA>B>OD.
Возьмем интерпретацию / = {А, ~ В, С, D]. Множество S содержит единичный дизъюнкт ~ D ложный в /. Построим множество
S* = {~ A v Д ~ В v С v ~ A, A, ~ Q.
База множества S* содержит три элемента. Построим Pi-вывод D* дизъюнкта П из S*:
<~ A v В, А > -> Б;
<В,~ C,~Av~BvO^>~A;
<~ А, А> -> П.
На рис. 21.15 изображено дерево, соответствующее PI - опровержению D* в S*. Исследуя каждый дизъюнкт построенного вывода, построим по описанным правилам Pi-опровержения D в S".
<~ Av B,~ D,Dv А>-+ В <~Д0у~С>-»~С
<В, ~ С, ~ Av ~ Bv О ^>~ А
<~ А, ~ D, D v А > -> П.
Рис. 21.15. Построение семантического опровержения для S*
На рис. 21.16 изображено дерево, соответствующее PI - опровержению D в S. В нем содержатся те элементы, которые были добавлены при исследовании вывода D *.
Рис. 21.16. Восстановленое семантическое опровержение для S*
Теперь предположим, что множество S не содержит единичного дизъюнкта, ложного в /. Выберем наименьший элемент Z и поступим следующим образом: в качестве L выберем либо Z, либо ~ Z, т. е. тот литерал, который ложен в /. Множество S* строим следующим образом: вычеркиваем все дизъюнкты, содержащие ~ L, из оставшихся дизъюнктов вычеркиваем дизъюнкт L. Так как S— противоречиво, то противоречивым будет и построенное множество S*. База множества S* содержит не более, чем «элементов, поэтому по индукционному предположению существует Pi-опровержение D\ в S*. Пусть Z> 2 — вывод, полученный из D\ возвращением литерала L в те дизъюнкты, из которых он был вычеркнут. Вывод Z>2 также является семантическим выводом, т. к. L — минимальный литерал, ложный в /. Семантический вывод Z>2 является выводом в S дизъюнкта D или дизъюнкта L. В первом случае теорема доказана.
Рассмотрим случай, когда DI является семантическим выводом в S дизъюнкта L: Z\, Zi, ..., L. Исследуем множество дизъюнктов S u {L}. Это множество содержит единичный дизъюнкт, ложный в интерпретации /. По доказанному ранее (вариант 1) существует семантический вывод D$ дизъюнкта П из множества 5u{Z}: Т\, Т 2 , ..., Т т <-» П.
Выбираем наименьшее у, такое, что 7} совпадает с L. Рассматриваем вывод L в S: Z\, Zj, ..., L. Так преобразованный вывод D$ будет Pi-выводом П из множества дизъюнктов S. Теорема доказана.
Пример построения семантического опровержения: вариант 2
Рассмотрим множество дизъюнктов:
S= (~ Av Bv С, ~CvAvB,~Av~C, Av Bv С, ~ В].
Выберем интерпретацию / = {~ А~ В, Q, определим порядок О В > А. Рассматриваемое множество S не содержит единичного дизъюнкта ложного в /. Выберем наименьший элемент А, он ложен в 7. Множество S* строим следующим образом: вычеркиваем все дизъюнкты, содержащие ~ А, из оставшихся дизъюнктов вычеркиваем дизъюнкт А:
S* = {~ Cv В, В У С, ~ В].
Так как S противоречиво, то противоречивым будет и построенное множество S*. Семантическое опровержение D\ в S*:
<В v ~ С, В v О -> В;
<В, ~ В> -» П.
При построении вывода DI возвращаем литерал А в те дизъюнкты, из которых он был вычеркнут:
<^v5v~C, Av Bv О -*Av В;
<А v В, ~ В > -» А.
Рассмотрим множество 5 и {А}, в нем есть единичный дизъюнкт А, ложный в интерпретации /. Следовательно, можно построить PI-опровержение D 3 в Sv{A}:
<A,~Av~O->~C.
<~ С, A, Bv Cv ~ A >-» В; <В,~В>-^П.
Преобразовывая Pi-опровержение DI, построим Pi-вывод дизъюнкта из множества дизъюнктов S:
<AvBv~C,AvBvO->AvB;
<А v В, ~ В > -» А;
<А, ~ A v ~ О -> ~ С;
<~ С, Л, Я v С v ~Л > -> #
<В,~В>->П.
1. Постройте семантическое опровержение для задачи о формировании экипажа при заданной интерпретации /= {- С, М,~ D}.
2. Постройте семантическое опровержение для задачи о поиске острова сокровищ при определенном порядке R О А> В > D> E> X> Y> Z.
3. Постройте семантическое опровержение для задачи об автомобилях.
1. Напишите сценарий, который по заданному множеству дизъюнктов S и интерпретации строит два множества дизъюнктов: в первое множество включаются все дизъюнкты, истинные в заданной интерпретации, во второе — ложные.
2. Напишите сценарий, который по заданному множеству дизъюнктов S, интерпретации / и порядку Р строит семантическое опровержение в S.
Рассмотрим некоторые частные случаи семантической резолюции.
Дизъюнкт называется положительным, если его литералы не содержат знаков отрицания, например, следующие дизъюнкты положительны:
A, A v С, В v С v А.
Дизъюнкт называется отрицательным, если все его литералы содержат знаки отрицания, например, следующие дизъюнкты отрицательны:
~А,~АУ ~ с,~ВУ~СУ~А.
Дизъюнкт называется смешанным, если он не является ни положительным, ни отрицательным, например:
~ Av С, 5 v С v ~ Л.
Положительной гиперрезолюцией называется семантическая (Pi-резолюция), в которой любой литерал интерпретации содержит знак отрицания. Гиперрезолюция называется положительной, потому что все
Е]
и PI-резольвенты при такой интерпретации положительные дизъюнкты. Положительная гиперрезолюция является частным случаем семантической резолюции.
Рассмотрим следующую задачу. При расследовании дела о хищении установлено:
Спрашивается, виновен ли В1
Запишем известные факты и предполагаемое следствие с помощью формул исчисления высказываний:
Построенное множество дизъюнктов будет иметь вид:
S = {A v В v С, ~ A v В v С, ~ С, ~ В}.
Зададим порядок Р. А > В >С. Рассмотрим интерпретацию /= {~ А,~ В,~ С]. Исходное множество б 1 разбивается на два, Zj и 1,2, следующим образом:
I, = {~ A v В v С, ~ С, ~ В};
£ 2 = (A v В v Q. Построим вывод дизъюнкта П из S:
<AvBvC,~AvBvO->BvC;
<5v С, ~ В> -^ ~ С;
<С, ~ О -> П.
Вывод является положительной гиперрезолюцией, все Е/ в семантическом конфликте положительны, любая семантическая резольвента также положительна.
Дерево вывода для положительной гиперрезолюции представлено на рис. 21.17. Положительная резолюция соответствует построению вывода, начиная с аксиом.
Рис. 21.17. Положительная гиперрезолюция для задачи о расследовании
Если же на множестве элементов задан порядок Р. О А > В, то Pi-опровержение будет следующим:
<Av Bv С, ~ О -> Л v Д
<Av В, -AvBvO^BvC;
<В v С, ~ О -» В;
<В,~В>^>
П.
Постройте семантическое опровержение, являющееся положительной гиперрезолюцией, для задач:
1. Напишите сценарий, который по заданному множеству дизъюнктов S строит семантическое опровержение, являющееся положительной гиперрезолюцией.
2. Напишите сценарий, который по заданному множеству дизъюнктов S и семантическому выводу определяет, является ли вывод положительной гиперрезолюцией.
Отрицательной гиперрезолюцией называется семантическая (Pi-резолюция), в которой любой литерал интерпретации не содержит знак отрицания. Гиперрезолюция называется отрицательной, потому что все
Е/
и Pi-резольвенты при такой интерпретации — отрицательные дизъюнкты. Отрицательная гиперрезолюция является частным случаем семантической резолюции.
Отрицательная гиперрезолюция для задачи о расследовании
В предыдущем примере исследовалось множество дизъюнктов: S- {A v В v С, ~ A v В v С, ~ С, ~ В].
Зададим порядок Р. А > В > С. Рассмотрим интерпретацию / = {А, В, Q. Исходное множество S разбивается на два, Zj и 1,2, следующим образом:
Z] = {A v В v С, ~ A v В v Q; 2 2 = {~ С, ~ В].
Построим вывод дизъюнкта П из S, который в данном случае будет отрицательной гиперрезолюцией:
<~ В, ~ С, ~ A v В v О -» ~ А; <~ А, ~ Я, ~ С, A v В v О -> П.
Дерево вывода для отрицательной гиперрезолюции представлено на рис. 21.18 и, как видно, вывод строится с отрицания заключения. Допустив, что заключение ложно, выводится противоречие из этого допущения.
Рис. 21.18. Отрицательная гиперрезолюция для задачи о расследовании
Постройте семантическое опровержение, являющееся отрицательной гиперрезолюцией, для задач:
1. Напишите сценарий, который по заданному множеству дизъюнктов S строит семантическое опровержение, являющееся отрицательной гиперрезолюцией.
2. Напишите сценарий, который по заданному множеству дизъюнктов
S
и семантическому выводу, определяет, является ли вывод отрицательной гиперрезолюцией.
Как и рассмотренные стратегии, стратегия поддержки направлена на то, чтобы не порождать лишние дизъюнкты.
Рассмотрим множество дизъюнктов S. Подмножество Т множества S называется множеством поддержки, если множество S-Т выполнимо.
Резолюцией с поддержкой называется резолюция, примененная к двум дизъюнктам, не принадлежащим одновременно множеству S- Т.
Вывод с поддержкой — это вывод, в котором любая резолюция — это резолюция с поддержкой.
Опровержение с поддержкой — это вывод с поддержкой дизъюнкта П.
Рассмотрим следующее множество дизъюнктов:
S= {С v Л/v Д ~ Cv Л/v Д Mv~ D, ~ Mv Д ~ Dv С, ~ D].
В качестве множества Г возьмем множество Т = {~ Л/v Д ~ D v Q. Множество S— Т состоит из дизъюнктов
S-T={Cv Mv D, ~ Cv Mv D, Mv~ D, ~ D}.
Оно выполнимо, для того чтобы убедиться в этом, достаточно выбрать интерпретацию, в которой литерал М истинен, а литерал Z) ложен. Множество Т является множеством поддержки для S. Следующий вывод представляет собой опровержение с поддержкой:
<Cv Mv Д ~ Л/v D> -> Cv Д
<~ Cv Mv D,~ MvD>->.~ Cv D;
<CvD,~CvD>^D;
<~ Д D > -> П.
Теорема о полноте метода поддержки
Пусть S —. противоречивое множество дизъюнктов, Т — подмножество S, такое, что S- Т выполнимо. Существует вывод с поддержкой дизъюнкта П из множества S, в котором Т 1 является множеством поддержки.
Доказательство.
Так как множество б
1
-Г выполнимо, то существует интерпретация /, в которой оно истинно. Будем рассматривать эту интерпретацию. Выберем любое упорядочивание
Р
для элементов базы. По теореме о полноте метода семантической резолюции существует Pi-вывод
D
дизъюнкта П из множества
S.
Рассмотрим произвольный семантический конфликт, порождающий семантическую резольвенту вывода
D: <Е\, EI,
...,
Eg, N>
для
g >
1. Все дизъюнкты
EJ
ложны в интерпретации /, поэтому в семантическом конфликте при построении резольвенты
RJ +
1 по дизъюнктам
R/
и
EJ
оба дизъюнкта не принадлежат одновременно множеству
S-T.
Следовательно, по любому семантическому конфликту может быть построен вывод с поддержкой. Теорема доказана.
Применение теоремы в задаче формировании экипажа
В задаче о формировании экипажа было построено и исследовалось следующее множество дизъюнктов:
S={CvMvD, ~ Cv Mv D, Mv~ D, ~ Mv D, ~ D v C, ~ D}.
Рассмотрим множество Т = {~ M v D, ~ D v С, ~ D}. Для того чтобы убедиться, что оно является множеством поддержки, достаточно показать, что множество
S-T= {Cv Mv Д ~ Cv Mv Д Mv ~ D}
выполнимо. Все дизъюнкты множества S- Т истинны в любой интерпретации, в которой истинен литерал М. Рассмотрим интерпретацию 7 = = {С, M, D}, зададим порядок О М> D. Мы можем построить следующий семантический вывод дизъюнкта П из множества S:
<~ D, ~ MvD> -» ~ М; <~ М, ~ D, ~ С v M v D > -» ~ С; <~ С, ~ М, ~ Д Cv Mv D> -> П.
По только что построенному семантическому выводу может быть построен следующий вывод с поддержкой:
<~ Д ~MvD>->~ M; <~ М, ~ Cv Mv D> -» ~ Cv Д
<~ Д ~ Cv Z)>->~ С;
<~ С, Cv Mv D> -» Mv Д
<~ M, Mv D>-* D;
<~ Д D > -» П.
Постройте вывод с поддержкой для задач: П о поиске острова сокровищ; П об автомобилях.
1. Напишите сценарий, который по заданному множеству дизъюнктов S строит вывод с поддержкой.
2. Напишите сценарий, который по заданному множеству дизъюнктов S и выводу определяет, является ли вывод выводом с поддержкой.
| Назад | Содержание |