Игошин Математическая логика и теория алгоритмов (1019110), страница 101
Текст из файла (страница 101)
Универсум Эрбрана, вообще говоря, бесконечен, но счетен. Например, если задано следующее множество формул (дизьюнктов) Ю = (Р(х) м Яа) ч —,РЯа)), — О(Ь) м РМх, у)Я, имеющее множество индивидов (а, Ь) и множество функциональных символов (Г, я), то его универсум Эрбрана представляет собой бесконечное множество Н(5) = (а, Ь, Ла), у(Ь), д(а, а), д(а, Ь), я(Ь, а), я(Ь, Ь), Я/"(а)), ...). 405 Второй пример: пусть в формулы из Я входят константы (индивиды) а, Ь, с, предметные переменные х, у, г, одноместная пре дикатная переменная Р и двухместная предикатная переменная (з Тогла /г(5) = (а, Ь, с).
Для построения эрбрановской интерпретации множества формул 5 нужно далее приписать значения истинности каждой конкретизации предикатных переменных на Р(х) и 0(у, г) на универсуме Эрбрана. Перечислим сначала все такие конкретизации: Р(а), Р(Ь), Р(с), Д(а, а), 0(а, Ь), 0(а, с), ЯЬ, а), 0(Ь, Ь), 0(Ь, с), 0(с, а), 0(с, Ь), 0(с, с). (Совокупность всех этих конкретизаций называется эрбрановской базой.) Каждому элементу этой базы нужно теперь приписать значение истинности 0 или 1, Поскольку элементов в базе 12, то, как мы знаем, это можно сделать 2'г = 4096 различными способами. Таким образом, мы получим 4096 эрбрановских интерпретаций данного множества формул. Форма правила резолюции в логике предикатов остается той же самой, что и в логике высказываний. Но в формулах логики предикатов содержатся предметные переменные, которых не было в формулах логики высказываний, и применение данного правила здесь несколько усложняется.
В этом случае над формулами логики предикатов производится еще одна процедура (после того, как из них после их сколемизации образовано множество дизъюнктов)— процедура унификации предметных переменных. Суть этой процедуры состоит в том, что в данных формулах некоторые предметные переменные заменяются конкретными предметами (индивидами), чтобы для формул, к которым нельзя было раньше применить правило резолюций, теперь это стало возможным.
Например, если к формулам Р(а) м 0(а, Ь) и 0(х, у) м А(х, у) нельзя применить правило резолюций, то после замены (подстановки) во второй формуле х на а и у на Ь получаем формулы Р(а) м — 0(а, Ь) и 0(а, Ь) м -Л(а, Ь), к которым это правило применимо, и оно дает формулу (резольвенту) Р(а) м -Я(а, Ь). (Отметим, что к формулам Р(а) г — 0(Ь, с) и Д(с, с) г .К(Ь, с) правило резолюции не применимо, — говорят, что они не резольвируют.) Подстановку г в х обозначим (г/х).
В случае выполнения множества подстановок (г,/хп ..., г„/х„) необходимо соблюдение ряда условий: а) х; является переменной, а г, — термом (константой, переменной, символом функции), отличным от хб б) для любой пары подстановок г;/х; и г/х. в правых частях символов / не содержатся одинаковые переменные. Как и в исчислении высказываний, в исчислении предикатов правило резолюции, примененное к формулам Р(а) и -Р(а), дает пустую формулу. Это означает, что исходное множество формул Рь ..., Г„, — б противоречиво, а значит, формула б выводима из формул Гп ..., Г . Сточки зрения семантики возможность выведения пУстой формулы означает, что нельзя построить эрбрановскую модель множества формул Рп ..., Р, — 6.
406 Наконец, о методе резолюций для доказательства теорем исчисления лредикавов. Для того чтобы автоматизировать процесс доказательства того, что формула 6 выводима из формул Гь ..., Г, было бы хорошо найти эффективный алгоритм, основывающийся на правиле резолюции, который позволял бы обнаруживать противоречивость множества формул Гь ..., Г, —,6.
Представим себе, что существует некая активная сила (человек или машина), которая по случайному закону применяет правило резолюции к формулам из множества (Гн ..., Г, — 6). После каждого выполнения резолюции получающаяся резольвента добавляется в это множество. Если будет сгенерирована пустая формула, то это и будет означать, что исходное множество формул противоречиво, и тогда эта активная сила прекратит свое действие. Если 6 выводима из Рь ..., Г, то множество формул (Рь ..., Г, — 6) действительно противоречиво, и активная сила рано или поздно сгенерирует пустую формулу и тем самым обнаружит эту противоречивость. Тем не менее в процессе работы может быть сгенерировано огромное количество резольвент. Поэтому для создания эффективного алгоритма поиска пустой формулы необходимо наложить ограничения на данный процесс и направить его активность на участки, которые с наибольшей вероятностью могут привести к появлению пустой формулы. Таким образом, при использовании метода резолюций возможна не одна стратегия поиска решения задачи, и важнейшей проблемой при этом является проблема эффективности алгоритма поиска доказательства.
Разработано большое число стратегий поиска доказательства методом резолюций (или, как говорят, исчисления резолюций), использующие, в частности, различного рода ограничения на вид исходных дизъюнктов (наиболее распространены так называемые дизъюнкты Хорна). Каждая из этих стратегий обладает своими преимуществами. Причем для одной и той же теоремы (формулы) некоторые стратегии могуг работать хорошо, а другие — плохо. С другой стороны, одна и та же стратегия лля одних теорем работает хорошо„а других — плохо. Рассмотрим подробнее так называемую нисходящую (или обратную) сглратегию на следующем конкретном и р и м е р е. Пусть имеются формулы: Р(а) ч — Д(а, Ь), Д(х, у) ч -А(х, у), Б(Ь), Я(а, Ь). Требуется выяснить, является ли формула Р(а) следствием перечисленных.
Сначала добавляем к данному множеству формул отрицание доказываемой формулы. В результате получаем следующее множество формул: (1): Р(а) ~ -О(а, Ь); (2): О(х, у) ~ — Р(х, у); (3): о(Ь); (4): А(а, Ь); (5): — Р(а). 407 Действие данного алгоритма метода резолюций будет сфокусировано на следствиях добавления формулы (5) к данному множеству формул (1) — (4). Алгоритм характеризуется следующими двумя требованиями: в первой выполняемой резолюции следует использовать только что добавленную формулу (5); в каждой последующей резолюции должна участвовать резольвента предыдущей резолюции (это предотвращает хаотическое «блуждание» алгоритма и порождение им необозримого количества «лишних» формул).
Согласно первому требованию на первом шаге применяем правило резолюции к формулам (5) и (1), которые резольвируют друг с другом. В результате получаем формулу (6): — О(а, Ь). Согласно второму требованию на следующем шаге должна участвовать формула (6). Она резольвирует с формулой (2). Результатом будет формула (7): — Я(а, Ь). (Обратите внимание на то, что в формуле (2) была предварительно проведена унификация предметных переменных с помощью подстановки а/х, Ь/у.) Формула (7) резольвирует с формулой (4). Их резольвентой является пустая формула. Это означает, что множество формул (1) — (5) противоречиво, что, в свою очередь, означает, что формула Р(а) является следствием формул (1) — (4). Рассмотренная стратегия метода резолюций является нисходящей, так как она начинает процесс решения с отрицания заключения, а далее в процессе решения используются остальные исходные формулы, что продолжается до тех пор, пока не будет выведена пустая формула.
Данная стратегия решения называется также стратегией поиска «сначала вглубь», поскольку результат последней резолюции всегда используется в следующей за ней резолюции. 5 40. От математической логики к логическому программированию Здесь будет кратко рассказано о языке логического программирования ПРОЛОГ, возникновение и развитие которого непосредственно связаны с открытием метода резолюций для доказательства теорем в логике, рассмотренного в предыдущем параграфе.
Его название происходит от слов РКОкгагпгп(пк 1п 1.ОО(с, т.е. ПРОграммирование в ЛОГике, или ПРОграммирование при помощи ЛОГики. В его основу положен математический аппарат логики предикатов 1-го порядка и теории логического вывода. Возникновение языка ПРОЛОГ и его развитие. После того как Робинсон в 1965 г. открыл правило вывода, названное им правилом резолюции, значительно активизировались работы по созданию автоматизированного метода доказательства теорем через опровержение. Первоначально попытки создания алгоритма решения задач, 408 базирующегося на правиле резолюции, оказывались успешными только лля очень небольших задач.
Существенно усовершенствовали такие алгоритмьз Лавленд, Ковальски и Куэнер, разработав метод устранения моделей (1968) и метод селектирующей функции (1971). В 1974 г. Ковальски первым предложил метод, в соответствии с которым логический язык (именно язык логики предикатов) можно было бы использовать как язык программирования.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
