Дискуссионный математический форумМатематический форум

Математический форум Math Help Planet

Обсуждение и решение задач по математике, физике, химии, экономике

Теоретический раздел
Часовой пояс: UTC + 4 часа [ Летнее время ]
MathHelpPlanet.com RSS-лента Математического форума

Часовой пояс: UTC + 4 часа [ Летнее время ]


Применение компьютеров для доказательства теорем математической логики

Применение компьютеров для доказательства
теорем математической логики


Мы уже отмечали, что формальные аксиоматические теории с их четкими понятиями аксиом и правил вывода, казалось бы, созданы для того, чтобы их развитие поручить электронно-вычислительной машине. И конечно же самым первым претендентом на союз с компьютером является формализованное исчисление высказываний. Исторически так оно и произошло: первые теоремы, доказанные компьютером, были теоремы формализованного исчисления высказываний. В логике и компьютерных науках стали говорить об автоматическом, или механическом, или машинном доказательстве теорем. В настоящем параграфе сначала будет рассказано об одной из первых попыток применить компьютер для поиска доказательств математических теорем — о компьютерной программе "Логик-теоретик", созданной в первой половине 1950-х гг. в США.


Программа "Логик-теоретик" и программы, близкие к ней


В 1957 г. известные американские специалисты по информатике А.Ньюэлл, Г.Саймон, Дж. Шоу сообщили, что при помощи разработанной ими программы "Логик-теоретик" на электронно-вычислительной машине IBM-704 получены доказательства для ряда (38) теорем формализованного исчисления высказываний, содержащихся в известном труде Б.Рассела и А.Уайтхеда "Principia Mathematica" (1925–1927).


В память машины с самого начала было помещено пять аксиом исчисления высказываний Рассела — Уайтхеда и три правила вывода. Кроме того, программа составлена так, что каждая из уже доказанных теорем оставалась в памяти машины и могла использоваться для дальнейших доказательств. Алгоритм поиска доказательств имел так называемый эвристический характер. Под "эвристиками" здесь понимается выявление общих правил, позволяющих решить поставленную задачу без необходимости систематического перебора всех потенциально существующих вариантов. С помощью своей программы "Логик-теоретик" ее создатели попытались смоделировать процесс поиска такого доказательства человеком. В качестве доводов, подтверждающих, что программа моделирует человеческое мышление, приводились результаты сравнения записей доказательств теорем в виде программы с записями рассуждений "думающего вслух" человека.


В основу алгоритма программы "Логик-теоретик" были положены следующие три эвристических метода: метод подстановки, метод отделения (modus ponens) и метод целеобразования.


Метод подстановки предназначен для поиска среди исходных аксиом и ранее доказанных теорем такой, которую требуется доказать в данный момент. При этом программа пытается определить, какие переменные или подформулы в уже имеющейся формуле нужно заменить и на какие формулы, чтобы получить ту формулу, которую требуется доказать. Для этого программа выполняет подстановки одних формул в другие и осуществляет равносильные преобразования формул на основании наличия в своей памяти основных равносильностей алгебры высказываний (коммутативность, ассоциативность, идемпотентность конъюнкции и дизъюнкции, законы поглощения и де Моргана, выражение импликации через дизъюнкцию и отрицание и т.п.).


Сам поиск доказательства той или иной теоремы (формулы) осуществляется методами отделения и целеобразования. Метод отделения состоит в том, что доказываемая формула заменяется более простой, доказав которую мы затем доказываем исходную формулу. Если [math]F[/math] — теорема, подлежащая доказательству, то машина ищет аксиому или уже доказанную теорему вида [math]G\to F[/math]. Затем делается попытка решить подзадачу — доказать теорему [math]G[/math]. Если она окажется доказанной, то из двух теорем [math]G[/math] и [math]G\to F[/math] по правилу МР (modus ponens) оказывается доказанной и теорема [math]F[/math].


Метод целеобразования предусматривает многократное использование метода отделения. Например, при необходимости доказать теорему [math]F\to H[/math] машина ищет ранее доказанную теорему вида [math]F\to G[/math]. Если такая теорема найдена в памяти, то перед машиной встает новая подзадача — доказать теорему [math]G\to H[/math]. Если и ее доказательство найдено, то из этих импликаций выводится требуемая теорема [math]G\to H[/math].


Таким образом, общая идея алгоритма поиска доказательства заданной теоремы [math]F[/math] состоит в восстановлении цепочки-доказательства так называемым обратным ходом, отправляясь от самой формулы [math]F[/math] и восстанавливая ее вплоть до уже доказанных теорем или до аксиом. Процесс поиска предшествующих формул исключительно неоднозначен и, как бы он ни был организован, носит переборный характер. И успешность выбора той или иной формулы не может быть оценена локально, в момент выбора. Поэтому программа вынуждена перебирать варианты, заходить в тупики, проходить циклы, прежде чем она сможет найти правильный путь решения. Повышение эффективности процесса вывода — центральная проблема всех автоматизированных систем дедуктивного вывода.


Как уже отмечено, с помощью этой программы была доказана часть теорем исчисления высказываний из книги Рассела и Уайтхеда "Principia Mathematica". Например, первая из этих теорем имеет вид: [math](F\to\lnot F)\to\lnot F[/math]. Эту теорему машина доказала в четыре шага и напечатала результат на выводном устройстве через 10 с после начала работы программы. Доказывая теорему [math]\bigl(F\lor (G\lor H)\bigr)\to \bigl((F\lor G)\lor H\bigr)[/math], машина через 23 мин после начала работы объявила об исчерпании возможностей данной программы. Простая на вид, но сложная для доказательства теорема [math]\lnot(F\to G)\to\lnot F[/math] была доказана через 12 мин в пять этапов. На этом примере, кстати, наглядно Демонстрируются принципиальные преимущества эвристических методов: если бы та же машина использовала не эвристические, а лишь чисто переборные методы, то для доказательства последней теоремы ей потребовалось бы несколько тысяч лет машинного времени.


Создатели программы "Логик-теоретик" показали также, что их программа может не только доказывать известные теоремы исчисления высказываний, но и может выдвигать новые теоремы и стремиться к их доказательству.


Аналогичные исследования по проблеме машинного поиска логического вывода велись и в Советском Союзе. Наибольшую известность получили исследования Н.А.Шанина и его сотрудников. Решается такая проблема: в заданном конкретном формализованном исчислении высказываний требуется составить алгоритм, выясняющий для любых формул [math]F_1,F_2,\ldots,F_m[/math] и [math]G[/math] этого исчисления, выводима ли формула [math]G[/math] из формул [math]F_1,F_2,\ldots,F_m[/math], и при утвердительном ответе на этот вопрос искомый алгоритм должен строить (и это в проблеме главное) вывод формулы [math]G[/math] из формул [math]F_1,F_2,\ldots,F_m[/math]. Машинная программа, реализующая удовлетворяющий указанным требованиям алгоритм, работала на машине "Урал-4" — одной из лучших советских электронно-вычислительных машин первой половины 1960-х гг.


Отметим также работы американского программиста Ван Хао, который в 1959 г. составил три программы для доказательства теорем исчисления высказываний и исчисления предикатов, реализовав их на машине IBM-704. Первая из них позволила машине за 37 мин доказать более двухсот теорем из первых пяти глав упоминавшейся книги Рассела и Уайтхеда "Principia Mathematica", причем 12/13 этого времени было израсходовано на ввод и вывод данных, так что время, потраченное собственно на доказательство, составило менее 3 мин. По второй программе машина сама составляла формулы исчисления высказываний и выбирала из них нетривиальные теоремы, строя их доказательства. В течение 1 ч было образовано и проверено около 14 тыс. формул, из которых выделено около тысячи теорем.


Наконец, третья программа предназначалась для доказательства более 150 теорем следующих пяти глав "Principia Mathematica" для исчисления предикатов с равенством. В течение 1 ч машина нашла доказательства для 85 теорем, которые были стройнее и короче доказательств, приведенных Расселом и Уайтхедом.


Позже появились программы, которые для доказательства теорем формализованного исчисления высказываний стали эффективно использовать метатеорию, т. е. теоремы о теоремах формальной теории. Первой такой программой стала программа французского математика Ж.Питра, созданная в 1966 г. Использование метатеорем позволило осуществить наибольший глобальный обзор поиска и сконцентрировать внимание на наиболее важных направлениях, не загружая память несущественными результатами. Программа Ж. Питра работает с шестью формализованными исчислениями высказываний, базирующимися на системах аксиом Рассела, Лукашевича. Гильберта, Бернея и Шеффера. Она отыскивает все основные теоремы, причем иногда дает для них оригинальные доказательства. Программа умеет работать и на уровне предположений: ей задается конкретное выражение и требуется его доказать. Достоинство программы в том, что с ее помощью удалось доказать некоторые теоремы, которые не смог доказать ее создатель. Вот суждение об этом самого Лукашевича: "Нужно быть очень опытным и искусным в построении логических доказательств, чтобы вывести закон коммутативности [math]\bigl(P\to (Q\to R)\bigr)\to \bigl(Q\to (P\to R)\bigr)[/math] или даже закон упрощения [math]P\to (Q\to P)[/math]". Программа Ж. Питра эффективно доказывает оба этих утверждения в рассматриваемой аксиоматике.




Метод резолюций для доказательства теорем исчисления высказываний и исчисления предикатов


Этот метод, разработанный американским математиком Дж.Робинсоном [9.20] в 1965 г., способствовал значительному прогрессу в автоматическом доказательстве теорем. Корни этого метода лежат в исследованиях известного французского логика Ж. Эрбрана, который в 1930 г. доказал очень важную теорему, послужившую основой для предложенного им механического метода доказательства теорем. (Эрбран погиб в 1931 г. в возрате 23 лет в Альпах во время восхождения на одну из вершин.) Как известно, в исчислении предикатов каждая теорема является общезначимой формулой (т.е. истинной во всякой интерпретации). Следовательно, необщезначимая формула не может быть теоремой. Так вот, Эрбран предложил алгоритм, устанавливающий необщезначимость формулы и, следовательно, ее недоказуемость. Точнее, он предложил алгоритм для нахождения интерпретации, не удовлетворяющей данной формуле, т.е. интерпретации, на которой формула превращается в ложное высказывание. Если заданная формула в действительности была общезначимой, то такой интерпретации не находилось, и алгоритм Эрбрана устанавливал этот факт за конечное (может быть, большое) число шагов. Если же заданная формула в действительности не была общезначимой, то алгоритм Эрбрана не мог установить этого факта за конечное число шагов. Таким образом, при отсутствии в то время вычислительных машин алгоритм Эрбрана оказался весьма трудоемким для ручных вычислений и не получил практического применения.


С появлением вычислительных машин интерес к механическому доказательству теорем резко возрос. В 1960 г. эрбрановский алгоритм был реализован на ЭВМ, были сделаны попытки его усовершенствования, но полученные программы были все же малоэффективны. Значительный прогресс в деле автоматического доказательства теорем начался с открытия Робинсоном в 1965 г. принципа резолюций.


Робинсон пришел к заключению, что правила вывода, которые следует применять при автоматизации процесса доказательства теорем при помощи компьютера, не обязательно должны совпадать с правилами вывода, используемыми человеком. Он обнаружил, что общепринятые правила вывода, в частности правило modus ponens, специально выбраны "слабыми", чтобы человек смог индуктивно проследить за каждым шагом процедуры доказательства. Робинсон открыл более сильное правило вывода, которое он назвал резолюцией (или правилом резолюции). Это правило трудно поддается восприятию человеком, но эффективно реализуется на компьютере. Оно имеет следующий вид:


[math]G\lor F,\, H\lor\lnot F\vDash G\lor H.[/math]
(1)

Нетрудно проверить, что формула [math]G\lor H[/math] действительно является логическим следствием двух формул, стоящих слева. При этом говорят, что формула [math]G\lor F[/math] резольвирует с формулой [math]H\lor\lnot F[/math], a формула [math]G\lor H[/math] называется резольвентой формул [math]G\lor F[/math] и [math]H\lor\lnot F[/math]. Если при этом в условии отсутствует формула [math]G[/math] (или она тождественно ложна), то правило (1) принимает приведенный ниже вид (2). Если в условии отсутствует формула [math]H[/math] (или она тождественно ложна), то правило (1) принимает вид [math]G\lor F,\lnot F\vDash G[/math]. Наконец, в случае отсутствия и [math]G[/math] и [math]H[/math] говорят, что правило резолюции дает (порождает) пустую формулу. (Фактически это означает, что из [math]F[/math] и [math]\lnot F[/math] выводится любая формула.)


Сравнив правило резолюции (1) с правилом modus ponens: [math]F,\,F\to H\vDash H[/math], записанным в виде


[math]F,\, H\lor\lnot F\vDash H,[/math]
(2)

можно видеть, что первое является обобщением второго. Наконец, приведенное выше правило резолюции можно представить в виде:


[math]\lnot G\to F,\, F\to H\vDash\lnot G\to H,[/math]
(3)

и в таком виде оно совпадает с правилом цепного заключения.


Основываясь на подходящей системе аксиом и правиле резолюции как единственном правиле вывода, можно построить полное формализованное исчисление предикатов первого порядка.


Приступим теперь к описанию метода резолюций для доказательства теорем в формализованных исчислениях. Начнем с формализованного исчисления высказываний. Отметим прежде одну простую идею.


Пусть даны формулы [math]F_1,\ldots,F_m[/math] и [math]G[/math]. Нетрудно доказать, что формула [math]G[/math] будет логическим следствием формул [math]F_1,\ldots,F_m[/math] тогда и только тогда, когда формула [math]F_1\land\ldots\land F_m\land\lnot G[/math] является противоречием (т. е. тождественно ложна). В самом деле,


[math]F_1,\ldots,F_m\vDash G \Leftrightarrow\vDash (F_1\land\ldots\land F_m)\to G[/math]

(см., например, теорему 6.4). Далее, формула [math](F_1\land\ldots\land F_m)\to G[/math] будет тавтологией, если и только если ее отрицание [math]\lnot \bigl((F_1\land\ldots\land F_m)\to G\bigr)[/math] будет противоречием. Равносильными преобразованиями эта формула приводится к требуемой:


[math]\begin{aligned}\lnot \bigl((F_1\land\ldots\land F_m)\to G\bigr)&\cong \lnot \bigl(\lnot (F_1\land\ldots\land F_m)\lor G\bigr)\cong\\ &\cong \lnot (\lnot F_1\lor\ldots\lor\lnot F_m\lor G)\cong\\ &\cong F_1\land\ldots\land F_m\land\lnot G. \end{aligned}[/math]

Наконец, по теореме адекватности формализованного исчисления высказываний (теорема 16.7) имеем


[math]F_1,\ldots,F_m\vdash G \Leftrightarrow F_1,\ldots,F_m\vDash G.[/math]

Таким образом, доказательство выводимости формулы [math]G[/math] из формул [math]F_1,\ldots,F_m[/math] в формализованном исчислении высказываний сводится к доказательству тождественной ложности формулы [math]F_1\land\ldots\land F_m\land\lnot G[/math].


В свою очередь, чтобы доказать тождественную ложность формулы [math]F_1\land\ldots\land F_m\land\lnot G[/math], достаточно доказать, что из совокупности формул [math]F_1,\ldots,F_m,\lnot G[/math] логически следует любая формула. Для этого и служит метод резолюций. Он состоит в том, что к формулам из множества [math]\{F_1,\ldots,F_m,\lnot G\}[/math] применяется правило резолюции. Получаемые формулы (резольвенты) также включаются в это множество, и к ним также может применяться это правило вывода. Порождение резольвент происходит до тех пор, пока не будет получена пустая формула. Как было отмечено выше, это и будет означать, что исходное множество [math]\{F_1,\ldots,F_m,\lnot G\}[/math] формул противоречиво, а формула [math]F_1\land\ldots\land F_m\land\lnot G[/math] тождественно ложна.


Рассмотрим простой пример. Пусть [math]F_1 \equiv\lnot P\lor\lnot Q\lor R,\, F_2 \equiv P,\, F_3 \equiv Q,\, G \equiv R[/math]. Спрашивается, следует ли формула [math]G[/math] из формул [math]F_1,F_2,F_3[/math]. Рассматриваем множество формул:


[math]\begin{aligned}&\mathsf{(1)}\colon~ \lnot P\lor\lnot Q\lor R~ (\equiv F_1);\\ &\mathsf{(2)}\colon~ P~ (\equiv F_2);\\ &\mathsf{(3)}\colon~ Q~ (\equiv F_3);\\ &\mathsf{(4)}\colon~ \lnot R~ (\equiv\lnot G). \end{aligned}[/math]


Применяем к формулам (1) и (2) правило резолюции. Получаем:


[math]\mathsf{(5)}\colon~\lnot Q\lor R.[/math]


Теперь применяем правило резолюции к формулам (3) и (5). Получаем:


[math]\mathsf{(6)}\colon~R.[/math]


Наконец, применение правила резолюции к формулам (4) и (6) дает пустую формулу:


[math]\mathsf{(7)}\colon~\Box[/math] (где [math]\Box[/math] — символ пустой формулы).


Таким образом, формула [math]G[/math] является логическим следствием формул [math]F_1,F_2,F_3[/math].


Присмотревшись внимательнее к приведенному примеру, видим, что участвующие в нем формулы [math]F_1,F_2,F_3,\,G[/math] имеют специфический вид, что на практике конечно же имеет место не всегда. Специфичность их вида состоит в том, что все они являются (совершенными) дизъюнктивными одночленами. Поэтому, если заданы произвольные формулы [math]F_1,\ldots, F_m,\,G[/math], то нужно составить формулу [math]F_1\land\ldots\land F_m\land\lnot G[/math], привести ее равносильными преобразованиями к (совершенной) конъюнктивной нормальной форме: [math]F_1\land\ldots\land F_m\land\lnot G\cong D_1\land D_2\land\ldots\land D_k[/math], а затем применять метод резолюций к множеству [math]S=\{D_1,D_2,\ldots,D_k\}[/math] (элементы этого множества называются дизъюнктами данной совокупности формул).


Перейдем теперь к рассмотрению метода резолюций в логике предикатов, для чего собственно этот метод и был создан.


Каждая формула логики предикатов, которая участвует в доказательстве по методу резолюций, должна быть представлена в специальном стандартном виде. Первый шаг на пути к преобразованию формулы к такому виду — это приведение ее к предваренной нормальной форме, бескванторная часть которой приведена к конъюнктивной нормальной форме. Эта процедура была подробно рассмотрена нами ранее.


Например, применяя указанную процедуру к формуле


[math]\begin{aligned}(\forall & x)\bigl\{P(x)\to \bigl[(\forall y)(P(y)\to R(x,y))\land\lnot (\forall y)(Q(x,y)\to P(y))\bigr]\bigr\}\cong\\[2pt] &\cong (\forall x) \bigl\{\lnot P(x)\lor \bigl[(\forall y)\bigl(\lnot P(y)\lor R(x,y)\bigr)\land (\exists y)\bigl(\lnot (\lnot Q(x,y)\lor P(y))\bigr)\bigr]\bigr\}\cong\\[2pt] &\cong (\forall x) \bigl\{\lnot P(x)\lor \bigl[(\forall y)\bigl(\lnot P(y)\lor R(x,y)\bigr)\land (\exists y)\bigl( Q(x,y)\land\lnot P(y)\bigr)\bigr]\bigr\}\cong\\[2pt] &\cong (\forall x) \bigl\{\lnot P(x)\lor \bigl[(\forall y)\bigl(\lnot P(y)\lor R(x,y)\bigr)\land (\exists t)\bigl( Q(x,t)\land\lnot P(t)\bigr)\bigr]\bigr\}\cong\\[2pt] &\cong (\forall x) \bigl\{\lnot P(x)\lor \bigl[(\forall y)(\exists t)\bigl(\lnot P(y)\lor R(x,y)\bigr)\land \bigl( Q(x,t)\land\lnot P(t)\bigr)\bigr]\bigr\}\cong\\[2pt] &\cong (\forall x)(\forall y)(\exists t) \bigl\{\lnot P(x)\lor \bigl[\bigl(\lnot P(y)\lor R(x,y)\bigr)\land Q(x,t)\land\lnot P(t)\bigr]\bigr\}\cong\\[2pt] &\cong (\forall x)(\forall y)(\exists t)\bigl[\bigl(\lnot P(x)\lor\lnot P(y)\lor R(x,y)\bigr)\land \bigl(\lnot P(x)\lor Q(x,t)\bigr)\land \bigl(\lnot P(x)\lor\lnot P(t)\bigr)\bigr].\end{aligned}[/math]

Далее, производится так называемая сколемизация полученной формулы, целью которой является удаление всех кванторов существования. Эта процедура заключается в следующем. Если на первом месте в формуле стоит квантор существования, то стоящая под ним предметная переменная всюду в данной формуле заменяется некоторым конкретным предметом (индивидом), а сам квантор существования опускается. Например, для формулы [math](\exists x)(\forall y)(P(x,y))[/math] эта процедура дает [math](\forall y)(P(a,y))[/math]. Если перед квантором существования [math]\exists y[/math] стоят кванторы общности [math]\forall x_1,\forall x_2,\ldots,\forall x_k[/math], то выбирается новый k-местный функциональный символ [math]f[/math] , все [math]y[/math] в формуле заменяются на [math]f(x_1,\ldots,x_k)[/math], а квантор [math]\exists y[/math] опускается. Получаемая формула называется сколемовской нормальной формой для данной формулы. Например, для рассмотренной выше формулы эта процедура дает


[math]\begin{gathered}(\forall x)(\forall y)\Big[ \bigl(\lnot P(x)\lor\lnot P(y)\lor R(x,y)\bigr)\land \bigl(\lnot P(x)\lor Q(x,f(x,y))\bigr)\land\\ \land \bigl(\lnot P(x)\lor\lnot P(f(x,y))\bigr)\Big]. \end{gathered}[/math]

Получившиеся дизъюнктивные одночлены образуют множество дизъюнктов исходной формулы, которое, подобно тому как это было в исчислении высказываний, участвует в доказательстве по методу резолюций. Для вышерассмотренной формулы приходим к следующему множеству дизъюнктов:


[math]S= \bigl\{\lnot P(x)\lor\lnot P(y)\lor R(x,y),\, \lnot P(x)\lor Q(x,f(x,y)),\, \lnot P(x)\lor\lnot P(f(x,y))\bigr\}.[/math]

Выше мы установили, что для доказательства выводимости формулы [math]G[/math] из формул [math]F_1,\lnot,F_m[/math] в исчислении высказываний достаточно доказать тождественную ложность формулы [math]F_1\land\ldots\land F_m\land\lnot G[/math], т.е. противоречивость множества дизъюнктов [math]\{F_1,\lnot,F_m,\lnot G\}[/math]. Аналогичным способом можно действовать и в исчислении предикатов. Но здесь нужно попытаться построить модель множества формул [math]\{F_1,\lnot,F_m,\lnot G\}[/math], т.е. найти такую интерпретацию, при которой все бы эти формулы превратились в истинные высказывания. Если такая модель существует, то [math]G[/math] не может быть следствием формул [math]F_1,\lnot,F_m[/math]. Если же такой модели не существует, то [math]G[/math] является следствием формул [math]F_1,\lnot,F_m[/math]. Ясно, что в общем случае поиск такой интерпретации придется вести среди необозримо большого количества интерпретаций (в зависимости от вида формул [math]F_1,\lnot,F_m,\,G[/math]). Но оказывается, круг исследуемых интерпретаций все же можно значительно сузить. Достаточно рассматривать интерпретации не на всевозможных множествах, а на так называемом универсуме Эрбрана. Интерпретации, возникающие на универсуме Эрбрана, называются эрбрановскими интерпретациями.


Универсум Эрбрана для множества [math]S[/math] формул логики предикатов обозначается [math]H(S)[/math] и строится рекурсивно следующим образом:


1) множество всех индивидов из [math]S[/math] принадлежит [math]H(S)[/math]; если в [math]S[/math] их нет, то [math]H(S)[/math] приписывается произвольный индивид [math]a[/math];


2) если термы [math]t_1,\ldots,t_n[/math], принадлежат [math]S[/math], то [math]H(S)[/math] содержит также [math]f(t_1,\ldots,t_n)[/math], где [math]f[/math] — любой n-местный функциональный символ из [math]S[/math];


3) никаких других термов в [math]H(S)[/math] нет.


Ясно, что при выборе любой интерпретации, т.е. при произвольном приписывании значений истинности (0 или 1) простейшим (атомарным) формулам из [math]S[/math], никаких других объектов предметной области, помимо объектов из [math]H(S)[/math], не потребуется. В этом смысле [math]H(S)[/math] — наиболее общая область интерпретации формул из [math]S[/math], так что поиск модели множества формул S можно ограничить эрбрановскими интерпретациями, и если мы установим, что такой модели для множества [math]\{F_1,\lnot,F_m,\lnot G\}[/math] среди этих интерпретаций нет, то ее не будет существовать вовсе, а значит, [math]G[/math] будет следствием формул [math]F_1,\lnot,F_m[/math]. Если же модель множества формул [math]S[/math] существует, то она существует и среди ее эрбрановских интерпретаций. Универсум Эрбрана, вообще говоря, бесконечен, но счетен.


Например, если задано следующее множество формул (дизъюнктов)


[math]S= \bigl\{P(x)\lor Q(a)\lor\lnot P(f(a)),\, \lnot Q(b)\lor P(g(x,y))\bigr\},[/math]

имеющее множество индивидов [math]\{a,b\}[/math] и множество функциональных символов [math]\{f,g\}[/math], то его универсум Эрбрана представляет собой бесконечное множество


[math]H(S)= \bigl\{a,b, f(a), f(b), g(a,a), g(a,b), g(b,a), g(b,b), f(f(a)),\ldots\bigr\}.[/math]

Второй пример: пусть в формулы из [math]S[/math] входят константы (индивиды) [math]a,b,c[/math], предметные переменные [math]x,y,z[/math], одноместная предикатная переменная [math]P[/math] и двухместная предикатная переменная [math]Q[/math]. Тогда [math]H(S)= \{a,b,c\}[/math]. Для построения эрбрановской интерпретации множества формул [math]S[/math] нужно далее приписать значения истинности каждой конкретизации предикатных переменных на [math]P(x)[/math] и [math]Q(y,z)[/math] на универсуме Эрбрана. Перечислим сначала все такие конкретизации:


[math]\begin{gathered}P(a),~ P(b),~ P(c),~ Q(a,a),~ Q(a,b),~ Q(a,c),~ Q(b,a),\\ Q(b,b),~ Q(b,c),~ Q(c,a),~ Q(c,b),~ Q(c,c). \end{gathered}[/math]

(Совокупность всех этих конкретизации называется эрбрановской базой.) Каждому элементу этой базы нужно теперь приписать значение истинности 0 или 1. Поскольку элементов в базе 12, то, как мы знаем, это можно сделать [math]2^{12}=4096[/math] различными способами. Таким образом, мы получим 4096 эрбрановских интерпретаций данного множества формул.


Форма правила резолюции в логике предикатов остается той же самой, что и в логике высказываний. Но в формулах логики предикатов содержатся предметные переменные, которых не было в формулах логики высказываний, и применение данного правила здесь несколько усложняется. В этом случае над формулами логики предикатов производится еще одна процедура (после того, как из них после их сколемизации образовано множество дизъюнктов) — процедура унификации предметных переменных.


Суть этой процедуры состоит в том, что в данных формулах некоторые предметные переменные заменяются конкретными предметами (индивидами), чтобы для формул, к которым нельзя было раньше применить правило резолюций, теперь это стало возможным. Например, если к формулам [math]P(a)\lor\lnot Q(a,b)[/math] и [math]Q(x,y)\lor\lnot R(x,y)[/math] нельзя применить правило резолюций, то после замены (подстановки) во второй формуле [math]x[/math] на [math]a[/math] и [math]y[/math] на [math]b[/math] получаем формулы [math]P(a)\lor\lnot Q(a,b)[/math] и [math]Q(a,b)\lor\lnot R(a,b)[/math], к которым это правило применимо, и оно дает формулу (резольвенту) [math]P(a)\lor\lnot R(a,b)[/math]. (Отметим, что к формулам [math]P(a)\lor\lnot Q(b,c)[/math] и [math]Q(c,c)\lor\lnot R(b,c)[/math] правило резолюции не применимо, — говорят, что они не резоль-вируют.) Подстановку [math]t[/math] в [math]x[/math] обозначим [math]\{t\!\!\not{\phantom{|}}\,x\}[/math]. В случае выполнения множества подстановок [math]\{t_1\!\!\not{\phantom{|}}\,x_1,\ldots,t_n\!\!\not{\phantom{|}}\,x_n\}[/math] необходимо соблюдение ряда условий:


а) [math]x_{i}[/math] является переменной, а [math]t_{i}[/math] — термом (константой, переменной, символом функции), отличным от [math]x_{i}[/math];


б) для любой пары подстановок [math]t_{i}\!\!\not{\phantom{|}}\,x_{i}[/math] и [math]t_{j}\!\!\not{\phantom{|}}\,x_{j}[/math] в правых частях символов [math]\!\!\not{\phantom{|}}\,[/math] не содержатся одинаковые переменные.


Как и в исчислении высказываний, в исчислении предикатов правило резолюции, примененное к формулам [math]P(a)[/math] и [math]\lnot P(a)[/math], дает пустую формулу. Это означает, что исходное множество формул [math]F_1,\ldots,F_m,\lnot G[/math] противоречиво, а значит, формула [math]G[/math] выводима из формул [math]F_1,\ldots,F_m[/math]. Сточки зрения семантики возможность выведения пустой формулы означает, что нельзя построить эрбрановскую модель множества формул [math]F_1,\ldots,F_m,\lnot G[/math].


Наконец, о методе резолюций для доказательства теорем исчисления предикатов. Для того чтобы автоматизировать процесс доказательства того, что формула [math]G[/math] выводима из формул [math]F_1,\ldots,F_m[/math], было бы хорошо найти эффективный алгоритм, основывающийся на правиле резолюции, который позволял бы обнаруживать противоречивость множества формул [math]F_1,\ldots,F_m,\lnot G[/math]. Представим себе, что существует некая активная сила (человек или машина), которая по случайному закону применяет правило резолюции к формулам из множества [math]\{F_1,\ldots,F_m,\lnot G\}[/math]. После каждого выполнения резолюции получающаяся резольвента добавляется в это множество. Если будет сгенерирована пустая формула, то это и будет означать, что исходное множество формул противоречиво, и тогда эта активная сила прекратит свое действие. Если [math]G[/math] выводима из [math]F_1,\ldots,F_m[/math], то множество формул [math]\{F_1,\ldots,F_m,\lnot G\}[/math] действительно противоречиво, и активная сила рано или поздно сгенерирует пустую формулу и тем самым обнаружит эту противоречивость. Тем не менее в процессе работы может быть сгенерировано огромное количество резольвент. Поэтому для создания эффективного алгоритма поиска пустой формулы необходимо наложить ограничения на данный процесс и направить его активность на участки, которые с наибольшей вероятностью могут привести к появлению пустой формулы.


Таким образом, при использовании метода резолюций возможна не одна стратегия поиска решения задачи, и важнейшей проблемой при этом является проблема эффективности алгоритма поиска доказательства. Разработано большое число стратегий поиска доказательства методом резолюций (или, как говорят, исчисления резолюций), использующие, в частности, различного рода ограничения на вид исходных дизъюнктов (наиболее распространены так называемые дизъюнкты Хорна). Каждая из этих стратегий обладает своими преимуществами. Причем для одной и той же теоремы (формулы) некоторые стратегии могут работать хорошо, а другие — плохо. С другой стороны, одна и та же стратегия для одних теорем работает хорошо, а других — плохо.


Рассмотрим подробнее так называемую нисходящую (или обратную) стратегию на следующем конкретном примере. Пусть имеются формулы:


[math]P(a)\lor\lnot Q(a,b),~ Q(x,y)\lor\lnot R(x,y),~ S(b),~ R(a,b).[/math]

Требуется выяснить, является ли формула [math]P(a)[/math] следствием перечисленных. Сначала добавляем к данному множеству формул отрицание доказываемой формулы. В результате получаем следующее множество формул:


\begin{aligned}&\mathsf{(1)}\colon~ P(a)\lor\lnot Q(a,b);\\ &\mathsf{(2)}\colon~ Q(x,y)\lor\lnot P(x,y);\\ &\mathsf{(3)}\colon~ S(b);\\ &\mathsf{(4)}\colon~ R(a,b);\\ &\mathsf{(5)}\colon~ \lnot P(a). \end{aligned}


Действие данного алгоритма метода резолюций будет сфокусировано на следствиях добавления формулы (5) к данному множеству формул (1)–(4). Алгоритм характеризуется следующими двумя требованиями: в первой выполняемой резолюции следует использовать только что добавленную формулу (5); в каждой последующей резолюции должна участвовать резольвента предыдущей резолюции (это предотвращает хаотическое "блуждание" алгоритма и порождение им необозримого количества "лишних" формул). Согласно первому требованию на первом шаге применяем правило резолюции к формулам (5) и (1), которые резольви-руют друг с другом. В результате получаем формулу


\mathsf{(6)}\colon~ \lnot Q(a,b).


Согласно второму требованию на следующем шаге должна участвовать формула (6). Она резольвирует с формулой (2). Результатом будет формула


\mathsf{(7)}\colon~ \lnot R(a,b).


(Обратите внимание на то, что в формуле (2) была предварительно проведена унификация предметных переменных с помощью подстановки [math]a\!\!\not{\phantom{|}}\,x,\, b\!\!\not{\phantom{|}}\,y[/math].) Формула (7) резольвирует с формулой (4). Их резольвентой является пустая формула. Это означает, что множество формул (1)–(5) противоречиво, что, в свою очередь, означает, что формула [math]P(a)[/math] является следствием формул (1)–(4).


Рассмотренная стратегия метода резолюций является нисходящей, так как она начинает процесс решения с отрицания заключения, а далее в процессе решения используются остальные исходные формулы, что продолжается до тех пор, пока не будет выведена пустая формула. Данная стратегия решения называется также стратегией поиска "сначала вглубь", поскольку результат последней резолюции всегда используется в следующей за ней резолюции.


Часовой пояс: UTC + 4 часа [ Летнее время ]


Яндекс.Метрика

Copyright © 2010-2016 MathHelpPlanet.com. All rights reserved