Игошин Математическая логика и теория алгоритмов (1019110), страница 100
Текст из файла (страница 100)
В 1960 г. эрбрановский алгоритм был реализован на ЭВМ, были сделаны попытки его усовершенствования, но полученные программы были все же малоэффективны. Значительный прогресс в деле автоматического доказательства теорем начался с открытия Робинсоном в 1965 г. принципа резолюций. Робинсон пришел к заключению, что правила вывода, которые следует применять при автоматизации процесса доказательства теорем при помощи компьютера, не обязательно должны совпадать с правилами вывода, используемыми человеком. Он обнаружил, что общепринятые правила вывода, в частности пра- 401 вило гподиз ролена, специально выбраны «слабыми», чтобы человек смог индуктивно проследить за каждым шагом процедуры доказательства.
Робинсон открыл более сильное правило вывода, которое он назвал резолюцией (или лравилом резолюции). Это правило трудно поддается восприятию человеком, но эффективно реализуется на компьютере. Оно имеет следующий вид: быГ, Н г —,Г~ 6чН. Нетрудно проверить, что формула 6 ы Н действительно является логическим следствием двух формул, стоящих слева. При этом говорят, что формула 6 ч Г резольвирует с формулой Н г — Г, а формула Сч Н называется резольвентой формул 6ч Ги Нч Г. Если при этом в условии отсутствует формула 6 (или она тождественно ложна), то правило (1) принимает приведенный ниже вид (2).
Если в условии отсутствует формула Н (или она тождественно ложна), то правило (1) принимает вид 6 г Г, — Г ~ 6. Наконец, в случае отсутствия и 6 и Н говорят, что правило резолюции дает (порождает) пустую формулу. (Фактически это означает, что из Ги Г выводится любая формула.) Сравнив правило резолюции (1) с правилом гподца ропепьч Г, Г-» Н Н, записанным в виде (2) Г,Н»-Г~Н, можно видеть, что первое является обобщением второго. Наконец, приведенное выше правило резолюции можно представить в виде: -,6-»Г,à — »Н -6 — »Н, (3) и в таком виде оно совпадает с правилом цепного заключения. Основываясь на подходящей системе аксиом и правиле резолюции как единственном правиле вывода, можно построить полное формализованное исчисление предикатов первого порядка.
Приступим теперь к описанию метода резолюций для доказательства теорем в формализованных исчислениях. Начнем с формализованного исчисления высказываний. Отметим прежде одну простую идею. Пусть даны формулы Гп ..., Г и 6. Нетрудно доказать, что формула 6 будет логическим следствием формул Г„..., Г„тогда и только тогда, когда формула Г, л ...
л Г л — 6 является противоречием (т.е. тождественно ложна). В самом деле, Гь ..., Г„~ 6 <=ь ~ (Г1 л ... л Г„) -ь 6 (см., например, теорему 6.4). Далее, формула (Г, л ... к Г ) -+ 6 будет тавтологией, если и только если ее отрицание -((Г, л ... л к Г ) — > 6) будет противоречием. Равносильными преобразованиями эта формула приводится к требуемой: 402 -1((Р1 л ... л Г ) — > 6) га -ъ(-з(Г~ л ...
л Р ) ч 6) н = —,(-,Р,ч .ч —,Г ч6)нР1л...лР л — 6. Наконец, по теореме адекватности формализованного исчисления высказываний (теорема 16.7) имеем Таким образом, доказательство выводимости формулы 6 из формул Уь ..., Р в формализованном исчислении высказываний сводится к доказательству тождественной ложности формулы Р, л ... л лр,„л- 6. В свою очередь, чтобы доказать тождественную ложность формулы Г, л ... л Г„л — 6, достаточно доказать, что из совокупности формул Р„..., Г„, — 6 логически следует любая формула. Для этого и служит метод резолюций. Он состоит в том, что к формулам из множества (Рь ..., Г, 6) применяется правило резолюции. Получаемые формулы (резольвенты) также включаются в это множество, и к ним также может применяться это правило вывода.
Порождение резольвент происходит до тех пор, пока не будет получена пустая формула. Как было отмечено выше, зто и будет означать, что исходное множество (Гн ..., Г, — 6) формул противоречиво, а формула Г, л ... л Г л -6 тождественно ложна. Рассмотрим простой пример. Пусть Г, =— -Рч-Цч А, Г, и Р, Гз = О, 6 = Я. Спрашивается, следует ли формула 6 из формул ЄÄРи Рассматриваем множество формул: (1): -Рч- Дч А (гя Р1); (2): Р (= Гз); (3): 0 (- =Рз)' (4): - Я (- =— 6).
Применяем к формулам (1) и (2) правило резолюции. Получаем: (5): — Д ч Я. Теперь применяем правило резолюции к формулам (3) и (5). Получаем: (6): Я. Наконец, применение правила резолюции к формулам (4) и (6) дает пустую формулу: (7): С) (где П вЂ” символ пустой формулы). Таким образом, формула 6 является логическим следствием формул Рь Рь Гз. Присмотревшись внимательнее к приведенному примеру, видим, что участвующие в нем формулы Рь Гь Ум 6 имеют специфический вид, что на практике конечно же имеет место не всегда. Специфичность их вида состоит в том, что все они являются (совершенными) дизъюнктивными олночленами. Поэтому, если заданы произвольные формулы Ен ..., Г„, 6, то нужно составить 403 формулу Р, н ...
н Р и — 6, привести ее равносильными преоб разованиями к (совершенной) конъюнктивной нормальной фор. ме: Г,н...нГ л-б=-Р,л Рзн...н Р„,азатемприменять метод резолюций к множеству 5 = [Р„Ръ ..., Р„) (элементы этого множества называются дизьюнктами данной совокупности формул) Перейдем теперь к рассмотрению метода резолюций в логике нредикатов, для чего собственно этот метод и был создан. Каждая формула логики предикатов, которая участвует в доказательстве по методу резолюций, должна быть представлена в специальном стандартном виде. Первый шаг на пути к преобразованию формулы к такому виду — это приведение ее к предваренной нормальной форме, бескванторная часть которой приведена к конъюнктивной нормальной форме. Эта процедура была подробно рассмотрена нами в 5 22 выше.
Например, применяя указанную процедуру к формуле (~ух)[Р(х) — > [(~гу)(Р(у) — > А(х, у)) н -(Оу)(Ц(х, у) — > Р(у))]) в, получаем =(Чх)[-Р(х) ч [(Фу)(- Р(у) ч А(х, у)) л (Лу)(-(- (г(х, у) ч Р(у)))]) в =- (Чх)[- Р(х) ч [(чу)(- Р(у) ч А(х, у)) л (Зу)(Ц(х, у) л-Р(у))]) в =- (ух)[-,Р(х) ч [(чу)(- Р(у) ч А(х, у)) л (Лг)((г(х, г) н — Р(г))]) в и (Мх)(-Р(х) ч ('Фу)(дг)[(- Р(у) ч А(х, у)) л (Ц(х, г) л -Р(г))]) в га (~Гх)('Фу)(Лг)[-Р(х) ч [(- Р(у) ч А(х, у)) л О(х, г) л -Р(г)]) в и (чх)(чу)(Лг)[(- Р(х) ч — Р(у) ч А(х, у)) н (-Р(х) ч Ц(х, г)) н л(-Р(х) ч -Р(г))]. Далее, производится так называемая сколемизация полученной формулы, целью которой является удаление всех кванторов существования.
Эта процедура заключается в следующем. Если на первом месте в формуле стоит квантор существования, то стоящая под ним предметная переменная всюду в данной формуле заменяется некоторым конкретным предметом (индивидом), а сам квантор существования опускается. Например, для формулы (Лх)(~гу)(Р(х, у)) эта процедура дает (чу)(Р(а, у)). Если перед квантором существования Лу стоят кванторы общности чхь ..., 'Фхм то выбирается новый /с-местный функциональный символ Г', все у в формуле заменяются на )"(хп ..., хг), а квантор Зу опускается.
Получаемая формула называется сколемовской нормальной формой для данной формулы. Например, для рассмотренной выше формулы эта процедура дает (Чх)('Фу)[(-,Р(х) ч —,Р(у) ч А(х, у)) л (-Р(х) ч Ц(х, Ях, у))) н л (. Р(х) ч — Р(г"(х, у)))]. Получившиеся дизъюнктивные одночлены образуют множество дизьюнктов исходной формулы, которое, подобно тому как это было в исчислении высказываний, участвует в доказательстве по методу резолюций. Для вышерассмотренной формулы приходим и следующему множеству дизъюнктов: 404 Х = (- Р(х) ч —,Р(у) ч А(х, у), Р(х) ~ Д(х, у(х, у)), — Р(х) ~ — Р(((х, у))). Выше мы установили, что для доказательства выводимости формулы 6 из формул Гь ..., Г в исчислении высказываний достаточно доказать тождественную ложность формулы Р; л ...
л Г„л — 6, т.е. противоречивость множества дизъюнктов (Гн ..., Г, 6). Аналогичным способом можно действовать и в исчислении предикатов. Но здесь нужно попытаться построить модель множества формул (Гь ..., Г, — 6), т.е. найти такую интерпретацию, при которой все бы эти формулы превратились в истинные высказывания. Если такая модель существует, то 6 не может быть следствием формул Гь ..., Г . Если же такой модели не существует, то 6 является следствием формул Рн ..., Г„. Ясно, что в общем случае поиск такой интерпретации придется вести среди необозримо большого количества интерпретаций (в зависимости от вида формул Гь ..., Г„, 6).
Но оказывается, круг исследуемых интерпретаций все же можно значительно сузить. Достаточно рассматривать интерпретации не на всевозможных множествах, а на так называемом универсуме Эрбрана. Интерпретации, возникающие на универсуме Эрбрана, называются эрбрановскими интерпретациями. Универсум Эрбрана для множества Юформул логики предикатов обозначается Н(о) и строится рекурсивно следующим образом: !) множество всех индивидов из о принадлежит Н(о); если в о их нет, то Н(Б) приписывается произвольный индивид а; 2) если термы гь ..., г„принадлежат о, то Н(5) содержит также Дгь ..., г„), где/' — любой и-местный функциональный символ из Х; 3) никаких других термов в Н(Б) нет.
Ясно, что при выборе любой интерпретации, т.е. при произвольном приписывании значений истинности (О или 1) простейшим (атомарным) формулам из о", никаких других объектов предметной области, помимо объектов из Н(Б), не потребуется. В этом смысле Н(Б) — наиболее общая область интерпретации формул из о', так что поиск модели множества формул о можно ограничить эрбрановскими интерпретациями, и если мы установим, что такой модели для множества (Гн ..., Г, — 6) среди этих интерпретаций нет, то ее не будет существовать вовсе, а значит, С будет следствием формул Рь ..., Г„. Если же модель множества формул о существует, то она существует и среди ее эрбрановских интерпретаций.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
