В основе метода автоматического (реализуемого программно) доказательства теорем лежит аппарат математической логики. Для простоты изложения мы приведем необходимое математическое обоснование метода и рассмотрим процесс доказательства на примере логики высказываний. В заключении мы обсудим специфические моменты, связанных с доказательством теорем в логике предикатов. Начнем изложение с основных определений и понятий логики высказываний.
Высказывание — это повествовательное предложение, о котором можно сказать истинно оно или ложно. Например, "Земля крутится" — это истинное высказывание, а "Земля плоская" — ложное. Говорят, что "истина" и "ложь" являются значениями истинности высказывания. Будем обозначать такие простые (атомарные) высказывания большими латинскими буквами, истину — единицей, а ложь — нулем.
Из простых высказываний можно составлять сложные посредством применения логических операций. Символы, обозначающие логические операции, называются связками. В качестве примера высказываний, содержащих логические операции можно привести следующие. Пусть X и Y — некоторые высказывания. Тогда:
| Высказывание | Название логической операции | Связка |
| "X и Y" | конъюнкция | & |
| "X или Y" | дизъюнкция | v |
| "не X" | отрицание | ¬ |
| "если X, то Y" | импликация | —> |
Истинность высказываний, получающихся в результате этих операций, определяется по следующим правилам. Конъюнкция высказываний истинна, если все операнды истинны. Дизъюнкция истинна, если хотя бы один операнд истинен. Отрицание истинно, если операнд ложен. Про импликацию X —> Y (если X, то Y) говорят, что X — посылка импликации, а Y — заключение импликации. Импликация ложна, если посылка импликации истинна, а заключение — ложно. Иначе импликация истинна.
Зависимость значения истинности сложного высказывания обычно изображают в виде таблицы истинности связок. Для основных логических операций эта таблица выглядит так.
| X |
Y |
X & Y |
X v Y |
¬X |
X —> Y |
0 |
0 |
0 |
0 |
1 |
1 |
0 |
1 |
0 |
1 |
1 |
1 |
1 |
0 |
0 |
1 |
0 |
0 |
1 |
1 |
1 |
1 |
0 |
1 |
Любое сложное высказывание можно привести к высказыванию, содержащему только логические операции дизъюнкции, конъюнкции и отрицания.
Формальная логика высказываний занимается анализом высказываний, при этом основное внимание уделяется форме высказывания в отвлечении от содержания. Формальным представлением высказывания является формула. Формула определяет форму высказывания, но не несет никакой информации относительно сути высказывания. Формулы состоят из букв и связок. Формула, не содержащая связок, называется атомарной формулой. Атомарные формулы будем обозначать буквами из конца латинского алфавита: U,V,W,X,Y и Z, помеченные или непомеченные нижним индексом. К числу атомарных формул относятся также 0 и 1. Неатомарные формулы будем обозначать буквами F или G (также допустим нижний индекс) или записывать в развернутой форме (через атомарные формулы и связки).
Чтобы судить об истинности формул, необходимо связать их с содержанием, т.е. выполнить интерпретацию формулы. Мы не можем, например, сказать, истинна формула W или ложна. Но если мы объявим, что W это высказывание "Земля вращается вокруг Солнца", что мы можем утверждать, что формула W истинна. Интерпретацию можно рассматривать как некоторую функцию, отображающую множество формул на множество высказываний. Обычно интерпретация, как функция, определяется лишь на множестве атомарных формул. Интерпретация неатомарных формул выполняется естественным образом как совместная интерпретация связок и атомарных формул, входящих в эту неатомарную формулу. Интерпретацию будем обозначать в виде малой латинской буквы j, за которой в скобках указывается обозначение интерпретируемой формулы. Например, j(F1).
В дальнейшем в интерпретации нас будут интересовать только значения истинности высказываний. Т.е. формулы мы будем интерпретировать в "истину" или "ложь". Тогда то, что формула X в интерпретации j истинна, можно записать в виде j(X)=1.
Одна из основных целей изучения логики состоит в получении формального аппарата для доказательства того, является ли данное утверждение следствием других.
Формула G называется логическим следствием формул F1,F2,...,Fk, если для любой интерпретации j из того, что j(F1)=j(F2)=...=j(Fk)=1 следует, что j(G)=1. |
Понятие логического следствия тесно связано с понятием выполнимости.
Множество формул {F1,F2,...,Fk} называется выполнимым, если существует интерпретация j такая, что j(F1)=j(F2)=...=j(Fk)=1. |
Проверку выполнимости множества формул {F1,F2,...,Fk} можно провести построением совместной таблицы истинности этих формул. Если найдется хотя одна строка, в которой в столбцах формул F1,F2,...,Fk стоят единицы, то это множество формул выполнимо. Если такой строки нет, то множество формул невыполнимо.
Теорема. Формула G является логическим следствием формул F1,F2,...,Fk тогда и только тогда, когда множество формул L={F1,F2,...,Fk, ¬G} невыполнимо. |
Доказательство. Пусть формула G является следствием множества формул F1,...,Fk. Предположим, от противного, что множество L выполнимо. Это означает, что существует интерпретация j такая, что j(F1)=...=j(Fk)=j(¬G)=1. Но если j(F1)=...=j(Fk)=1, то j(G)=1, поскольку G — логическое следствие формул F1,...,Fk. Полученное противоречие j(¬G)=1 и j(G)=1 доказывает, что множество формул {F1,...,Fk, ¬G} невыполнимо. Пусть теперь множество формул L невыполнимо. Рассмотрим интерпретацию j такую, что (F1)=...=j(Fk)=1. Поскольку L невыполнимо, то j(¬G)=0. Если j(¬G)=0, то j(G)=1. Следовательно, из равенств (F1)=...=j(Fk)=1 следует равенство j(G)=1. Это означает, что G — логическое следствие множества формул F1,...,Fk. |
Доказательство теорем сводится к доказательству того, что некоторая формула G (гипотеза теоремы), является логическим следствием множества формул F1,...,Fk (допущений). Т.е. сам текст теоремы может быть сформулирован следующим образом "если F1,...,Fk истинны, то истинна и G". Такой метод доказательства теорем называется методом резолюций.
Как было показано ранее, задача о логическом следствии может быть сведена к задаче о выполнимости. Формула G есть логическое следствие формул F1,F2,...,Fk тогда и только тогда, когда множество формул {F1,F2,...,Fk,¬G} невыполнимо. Метод резолюций как раз и занимается тем, что устанавливает невыполнимость такого множества формул.
Прежде, чем мы опишем сам метод, необходимо ввести еще ряд понятий.
Литералом называется атомарная формула или ее отрицание. Дизъюнктом называется дизъюнкция литералов. Дизъюнкт может состоять из одного литерала. Пустой дизъюнкт — это специальный дизъюнкт, не содержащий литералов. Будем обозначать его #. Считается, что пустой дизъюнкт ложен при любой интерпретации. Пустой дизъюнкт является, по сути, атомарной формулой 0, но в контексте метода резолюций принято пользоваться #. Литералы X и ¬X называются противоположными.
Метод резолюций основан на правиле резолюции.
Правило резолюции. Из дизъюнктов (X v F) и (¬X v G) выводим дизъюнкт (F v G). Или другими словами, дизъюнкт (F v G) является логическим следствием дизъюнктов (X v F) и (¬X v G). |
Т.е. если j(X v F)=1 и j(¬X v G)=1 для некоторой интерпретации j, то j(F v G)=1. Это легко доказать. Пусть j(X v F)=1 и j(¬X v G)=1. Тогда, если j(F)=1, то и j(F v G) = 1. Если же j(F)=0, то j(X) должно быть равно 1, поскольку j(X v F)=1. Но тогда j(¬X)=0. А следовательно, j(G)=1, так как j(¬X v G)=1. Но если j(G)=1, то и j(F v G) = 1.
Введем понятие вывода. Пусть S — множество дизъюнктов. Выводом из S называется последовательность дизъюнктов D1,D2,...,Dn такая, что каждый дизъюнкт этой последовательности принадлежит S или следует из предыдущих по правилу резолюций. Дизъюнкт D выводим из S, если существует вывод из S, последним дизъюнктом которого является D.
Применение метода резолюций основано на следующем утверждении, которое называется теоремой о полноте метода резолюций.
Теорема. Множество дизъюнктов логики высказываний S невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт. |
Сам метод резолюций можно сформулировать таким образом.
Метод резолюций. Для доказательства того, что формула G является логическим следствием множества формул F1,...,Fk метод резолюций применяется следующим образом. Сначала составляется множество формул {F1,...,Fk, ¬G}. Затем каждая из этих формул приводится к конъюнктивной нормальной форме (конъюнкция дизъюнктов) и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов S. И, наконец, ищется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул F1,...,Fk. Если из S нельзя вывести #, то G не является логическим следствием формул F1,...,Fk. |
Рассмотрим пример доказательства методом резолюций. Пусть у нас есть следующие утверждения:
Итак, докажем, что X3 является логическим следствием (X1 & X2) и (X1 —> X3). Сначала составляем множество формул с отрицанием доказываемого высказывания; получаем:
{(X1 & X2), (X1 —> X3), ¬X3}.
Теперь приводим все формулы к конъюнктивной нормальной форме и зачеркиваем конъюнкции. Получаем следующее множество дизъюнктов:
{X1, X2, (¬X1 v X3), ¬X3}.
Ищем вывод пустого дизъюнкта (в этом выводе третий и последний элементы получены по правилу резолюции, остальные являются элементами исходного множества дизъюнктов):
X1, (¬X1 v X3), X3, ¬X3, #.
Получили пустой дизъюнкт, значит утверждение о том, что яблоко вкусное верно.
Метод резолюций применим и к логике предикатов первого порядка (далее просто логика первого порядка). Однако, чтобы сделать метод рабочим, требуется внести ряд изменений и дополнений в версию для логики высказываний. Мы не будем здесь вдаваться в подробности. Отметим лишь те моменты, на которые следует обратить внимание при переходе от логики высказываний к логике первого порядка.
В исчислении первого порядка мы сталкиваемся с таким понятием как переменная. Поэтому правило резолюций надо дополнить возможностью делать подстановку. Грубо говоря, подстановкой называется множество равенств между переменными и термами. Подстановка называется унификатором некоторого множества атомарных формул, если в результате подстановки все атомарные формулы множества станут одинаковыми. Если множество унифицируемо, то существует, как правило, не один унификатор этого множества, а несколько. Среди всех унификаторов данного множества выделяют, так называемый, наиболее общий унификатор. Не будем здесь определять это понятие. Здесь нам важно лишь понять, что унификатор — это подстановка, которая делает элементы некоторого множества атомарных формул одинаковыми. Отметим, что существует метод получения наиболее общего унификатора для любого множества атомарных формул.
В этой терминологии правило резолюций для логики первого порядка можно записать так.
Правило резолюции. Из дизъюнктов (P(t1,...,tn) v F) и (¬P(u1,...,un) v G) выводим дизъюнкт (s(F) v s(G)), где s — наиболее общий унификатор множества {P(t1,...,tn), P(u1,...,un)}. |
Получившийся дизъюнкт (s(F) v s(G)) называют резольвентой.
В отличие от логики высказываний, в логике предикатов нам понадобится еще одно правило, которое называется правилом склейки..
Правило склейки. |
Получившийся дизъюнкт (s(P(t1,...,tn)) v s(F)) называют склейкой (то же касается и дизъюнкта с отрицанием).
Определение понятия вывода в логике первого порядка немного отличается от аналогичного определения в логике высказываний. Выводом из множества дизъюнктов S называется последовательность дизъюнктов D1,D2,...,Dn такая, что каждый дизъюнкт этой последовательности принадлежит S, или выводим из предыдущих дизъюнктов по правилу резолюций или по правилу склейки.
В остальном, метод резолюций для логики первого порядка ничем не отличается от метода для логики высказываний. Все сводится к невыполнимости множества дизъюнктов. А множество дизъюнктов S логики первого порядка невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт.
Трофимов И.В.
март 2005 г