Intel_Nils (526801), страница 48
Текст из файла (страница 48)
Мы будем говорить, что граф доказательства имеет вид лозы, если каждая его вершина либо является базовым предложением, либо непосредственно следует из базового предложения. (Такой граф будет деревом, но не все деревья имеют вид 0.4. Формьь доказательства с отфильтроваванием лозы. Это видно из примеров гл. 6, где граф рис. 6.3 имеет впд лозы, а граф, изображенный на рис. 6А, нет.) Если граф опровержения, имеющий вид лозы, существует, то для его построения достаточно резольвент лишь тех пар предложений, из которых хотя бы одно принадлежит В. Такое ограничение на резольвенции могло бы лечь в основу прекрасной стратегии очищения, если бы только быть уверенным, что для любого невыполнимого множества предложений существует граф опровержения, имеющий вид лозы.
К сожалению, стратегия очищения, основанная на графах в виде лозы, не полна; но одна очень похожая на нее стратегия полна. Чтобы убедиться, что для невыполнимого множества граф в виде лозы существует не всегда, рассмотрим множество !е (х) Ч Р (а) Я(х) Ч Р(х) -Я(х) у-Р(х) Я(х) ~/ Р(х) Из графа опровержения, представленного на рис. 8.1, видно, что это множество невыполнимо.
В графе опровержения, имеющем вид лозы, одно из предложений множества В должно быть вершиной, непосредственно предшествующей корневой вершине и!1. Но для образования пустого предложения нужна либо резольвента двух предложений, содержащих по одному литералу, либо два предложения, которые «факторизуются» ') к предложениям, содержащим по одному литералу. Ни один из элемент тов множества 5 не удовлетворяет этим требованиям, так что для 5 не может быть опровержения в виде лозы.
Из рис. 8.! видно, что одна из резольвенций производится между предложениями -Р(а) и Р(о) ~/ Р(х). Далее, в этом графе опровержения предложение Р(а) т' Р(х) предшествует предложению Р(а). Граф рнс. 8.1 служит примером графа с отфильтрованными предшествующими вершинами, нли графа в АЕ-форме. Мы будем говорить, что граф опровержения имеет АЕ-форму, если каждая вершина графа соответствует одному из следующих предложений: 1) базовому предложению; 2) предложению, непосредственно следующему за базовым; 3) предложению, непосредственно следующему за двумя не- базовыми предложениями А и В, из которых В предшествует А (отсюда термин — отфильтровывание предшествующих вершин).
Граф в виде лозы представляет собой частный случай графа в АЕ-форме: каждая нз его вершин соответствует либо ') См. стр. !96.— Прим. перев. л40 Гл. В. Методы поиска докаеательства в иевислеиии предикатов предложению 1), либо предложению 2). Базовое предложение С в графе, имеющем АР-форму, называется концевой вершиной, если любая другая вершина дерева либо является базовым предложением, либо следует за С.
Е(х) ~Р() о р(х) Р(а) к Р1х) р(х) пп Р и е. З.!. Граф оаровержеипк. Сформулируем без доказательства теорему, утверждающую, что для любого невыполнимого множества предложений всегда существует граф опровержения в АР-форме. Таким образом, стратегия очищения, основанная на поиске графов в АР-форме, полна, Теорема 8.1.'Пусть пт(п1!) — граф опровержения для невьтолнимого множества 5 предложений, а С вЂ” некоторое предложение из 5, появляющееся'в пт(п11). Тогда для 5 существует граф опровержения пт'(п!1) в АР-форме, для которого С служит концевой вершиной. 8лй Формы доказательства с отФильтровыааиием 241 Для многих графов частный случай опровержения в АР- форме, имеющий вид лозы, существует.' Дерево, изображенное на рис.
6.4, не имеет АР-формы, однако дерево опровержения для того же самого множества предложений с 0(х) ч' — Е1у) в качестве концевой вершины, показанное на рис. 8.2, имеет вид ()(м) ч -Е(У) „Е(а) ч В(м ' 8( ) ч С( ) С(а) ч - Е(У) В(а) -В(а) ч -Е(у) -с(с) ч Е(т)) Е(у) -С1с) Рис.
8.2. Дерево опровержения в виде лозы. лозы. Читатель может попытаться построить для этого множества предложений, но с иными концевыми вершинами, другие гра ы в АР-форме. ак как в теореме 8.1 утверждается, что для любого невыполнимого множества предложений существует граф опровержения в АР-форме, то перебор можно ограничить, отыскивая лишь опровержения такого вида. Назовем стратегией АР-формы стратегию очищения, реализующую это ограничение.
В ней применяются резольвенции по отношению к критерию отфильтровывания предшествующих вершин. Этот критерий можно 24з Гл. 8. Методы поиска доказательства в исчислении предикатов описать следующим образом. Сначала отметим, что при выборе концевой вершины для графа в АР-форме допускается некоторый произвол. Концевая вершина должна появляться в каком- нибудь графе опровержения, так что она выбирается из не.
которого подмножества К ~ 5, содержащего предложения, появляющиеся в каком-нибудь опровержении (например, в Л(х) -д(х) Н 8(х! 8(х) и г(х) т(х1 ч л(х) Ж (81 дг(81 — д(х) пм Рис, 8.3. Поиск опровержения с использованием Ар-стратегии.
К могут содержаться предложения, возникающие при отрицании теоремы, которую предстоит доказать). Тогда критерий, которому должна удовлетворять пара предложений (А, В) для того, чтобы ее можно было подвергнуть резольвенции в отношении АР-стратегии, таков: один элемент пары (А,В) принадлежит 5, а другой есть либо предложение из К, либо предложение, следующее за предложением из К, или один из элементов пары (А, В) предшествует другому. ' Обозначим через ЖАР(5) объединение множества 5 и множества всех резольвент всех пар из 5, допускаемых АР-стратегией. Положим, как обычно, АР ( АР ( ) АР к~АР ( ))' Согласно теореме 8.1, если множество 5 неудовлетворимо, то найдется такое п, что п11 еи ЯАР(5).
На рис. 8.3 показан результат применения АР-стратегии к простому неудовлетворимому множеству предложений. (В этом 8.7. Модельные стратегии примере К = 5.) На уровнях 1 и 2 выполнялись все допустимые резольвенции до тех пор, пока не было выведено на уровне 8 пустое предложение. Образованный такой процедурой граф в АР-форме отмечен жирными линиями. Он оказался лозой. 8.5. СТРАТЕГИЯ ПОДДЕРЖИВАЮЩЕГО МНОЖЕСТВА Стратегией поддерживающего множества называют стратегию, в которой выбирается такое непустое подмножество К исходного множества предложений 5, что множество 5 — К удовлетворнмо. Например, можно в качестве К взять множество предложений, возникающих из отрицания доказываемой теоремы.
Говорят, что предложения в К имеют поддержку. При поиске опровержения допустимыми считаются резольвенции лишь тех пар предложений, в которых по крайней мере одно имеет поддержку. Каждому предложению„построенному в результате резольвенции, также придается поддержка. Так как множество 5 — К удовлетворнмо, существует граф опровержения, имеющий АР-форму, у которого верхней вершиной служит один из элементов множества К.
Таким образом, стратегия поддерживающего множества полна, поскольку она допускает все резольвенции, допускаемые АР-стратегией (и, возможно, другие). 88. БОЛЕЕ ОГРАНИЧИТЕЛЬНЫЕ СТРАТЕГИИ В действительности АР-стратегию можно еще ограничить, сохранив при этом полноту. Одно из ограничений состоит атом, что если А предшествует В, то резольвенту для А и В можно строить лишь тогда, когда она является подслучаем подстановкового частного случая предложения В (Лавленд, 1969). Можно наложить также н другие ограничения, связанные со специальными типами резольвенций, называемыми слияниями (Эндрюс, 1968; Р(ейтс, Рафаэль, Харт, 1970). Конечно, при выборе стратегии следует иметь в виду, что затраты на дополнительные вычисления, требуемые для выбора соответствующих резольвенций, могут и не перекрыться экономией, вызванной уменьшением числа резольвенций, выполненных на самом деле в процессе перебора. В настоящее время судить об этом можно лишь на основании практического опыта.
8.7. МОДЕЛЬНЫЕ СТРАТЕГИИ Напомним, что в гл. 6 мы придали точный смысл интерпретации, задав значения истинности атомов в эрбрановской базе. Мы назвали такое задание значений истинности моделью. Так, если эрбрановская база состоит из атомов (Р(а, о), Р(а, а), 244 Гл. 8. Методе~ аоиска докаэательства в исеислении аредикатов Р(Ь, Ь), Р(Ь, а), Я(а), Я(Ь)), то одной из моделей может быть ( Р(а, Ь), Р(а,а), Р(Ь, Ь), Р(Ь,а), Я(а), е,т(Ь)). В общем случае моделью является множество (быть может, бесконечное) литералов, сконструированных исходя из эрбрановской базы таким образом, что каждый атом эрбрановской базы содержится в модели либо со знаком отрипания, либо без него (но не может быть и то и другое одновременна). По определению модель не удовлетворяет предложению С, если С имеет константный частный случай (полученный с помощью элементов универсума Эрбрана), принимающий значение Р при означивании на основе данной модели.
В противном случае говорят, что модель удовлетворяет предложению С. Обычно можно определить непосредственно, удовлетворяет ли данная модель М предложению С. Например, модель (-Р(а, Ь), Р(а, а), Р(Ь, Ь), Р(Ь, а), Я(а), О(Ь)) не удовлетворяет предложению Я(х) т Р(у, х), так как подстановка ((Ь, х), (а,у)) приводит к константному частному случаю со значением истинности Р. Эта модель удовлетворяет предложению ( Я(х) Ч Р(у,у)), так как ни одна из подстановок не приводит к константному частному случаю со значением истинности Р. Часто удается представить модель более компактно в виде списка литералов, у которых все константные частные случаи (на универсуме Эрбрана) имеют значение истинности Т.
При этом нужно проследить, чтобы не получилось противоречивого результата и чтобы каждому атому эрбрановской базы было присвоено значение истинности. Так, если множество есть Я(х) ~/ Р(а, г'(х)) Я (х) ~/ Р 0 (х), п) Р (х, г (х)) ~l )с (у) ег (а) то моделью может быть, например, множество (Я(х), Р(а,((х)), Р(х,Г(х)), РЯх),а), )с(х)), В терминах атомов эрбрановской базы эта модель представляет собой бесконечное множество М=Я(а), Я(~(а)), ес()Д(а))), ..., Я(а), Я(~(а), сто(((а))), ... Р (а, ~ (а)), Р (а, г Ц (а))), ..., Р Д (а), (() (а))), ...
..., Р(((а), а), Р(г Д(а)), а), ...). Заметим, что первое и четвертое предложения этой моделью не удовлетворяются, а второе и третье — удовлетворяются. Понятием модели можно воспользоваться для того, чтобы, ограничить число резольвенций, необходимых для нахождения В.т. Модельные етратегпи Е(л1 пи Р и с К4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
