Рассуждений.

Алгоритмы, эффективно распознающие достоверность

Не будем изучать всю более чем тысячелетнюю историю поиска эффективных алгоритмов доказательства теорем, и проводить сопоставительный анализ всех известных алгоритмов. Достаточно привести лишь те алгоритмы, которые нашли широкое практическое применение в искусственном интеллекте. Наиболее известным алгоритмом называется метод резолюций (резолютивный вывод). Он зародился в 1930 году (Эрбран), развитие и становление получил в 1965 году (Робинсон), широкое применение имеет с 70-х годов (Кольмрауер - язык Пролог для доказательства теорем) и до нашего времени.

Известно много вариантов применения метода резолюций, но самой высокой эффективностью он обладает в следующих условиях:

1).Когда целевая теорема преобразована в противоположную теорему;

2).Когда целевая теорема представлена в структуре приведенной конъюнктивной нормальной формы (ПКНФ) со следующей принци-пиальной особенностью: дизъюнкты в ПКНФ являются дизъюнктами Хорна. ПКНФ, удовлетворяющая 2-му требованию, называется канонической формой, имеющей вид:

(P₁ Ú P₂ Ú...)Ù(q₁Úq₂Ú...) Ù...Ù(r₁Ú r₂Ú...)Ùù (c₁Ú c₂ Ú...),

где, P_i, q_i, r_k -литеры посылок, а С_t- литеры заключения (понятия “противоположная теорема” и “ дизъюнкт Хорна” рассмотрим позже);

3).Когда при доказательстве целевой теоремы пользуются дедуктивным рассуждением, называемым обратной дедукцией, которое коренным образом отличается от прямой (классической) дедукции (об обратной дедукции – тоже позже);

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

а) Сущность метода резолюций.

Применение метода резолюций базируется на фундаментальном методе дедукции: множество формул дедуктивного рассуждения невыполнимо тогда и только тогда, ложь( Л ) является логическим следствием его (этого множества). Это же свойство можно сформу-лировать иначе:

Формула С является логическим следствием конечного множества Е тогда и только тогда , когда ЕÙùС не выполнимо. Это свойство дедуктивного рассуждения, вытекающее из его определения, широко известно как принцип дедукции.

В формальном представлении оно выглядит так:

Œ H ₁ , H₂...,H _n  C º Œ H₁ , H₂, ...,H _n ,ù C  Л ,

где метасимвол - - отношение логического следования,

H_i ( i= 1, n) - посылка в дедуктивном рассуждении, С- заключение в рассуждении.

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

Для порождений логических следствий будем использовать следующую схему рассуждений. Пусть А, В и Х - формулы.

Предположим, что две формулы ( AÚX) и ( BÚù X) - истинны. Если X- тоже истинна, то ù X – Л и тогда можно заключить, что B -истинна.

Наоборот, если X-ложна, то можно заключить, что A- ложна. Т.о., в обоих случаях ( AÚB)- истинна.

Получаем правило Œ AÚ X , BÚù X A Ú B , которое можно записать также в виде:

Œù X®A ,X ® B  A Ú B .

В том частном случае, когда X- высказывание , A и B - дизъюнкты, это правило называется правилом резолюций.

б) Сущность преобразования целевой теоремы в противоположную теорему.

В классической математике понятие “ противоположная теорема “ означает, что заключение противоположной теоремы является отрицанием заключения исходной теоремы, а посылки противоположной теоремы являются отрицанием посылок исходной теоремы. Например, A®B -исходная теорема , ù A ® ù B - противоположная теорема. Так как отрицание общезначимой формулы - противоречивая формула, то и доказывать следует противоречивость, а не общезначимость противоположной формулы.

Т.о., если исходная целевая теорема имеет вид:

( D₁ Ù D ₂ Ù ...Ù D _n ) ® C , (1)

где D_i - дизъюнкты Хорна, C- заключение теоремы, то, преобразуя формулу (1) по правилу 2 , получим новую формулу без импликации

( ù ( D₁Ù D₂Ù ...Ù D_n ) Ú C ). (2)

Преобразуя (2) в противоположную формулу, получим ПКНФ:

( D₁ Ù D₂ Ù... Ù D_n Ù ù C) (3)

ПКНФ (3) будет противоречива, если какой-либо дизъюнкт D_i или ù С- ложен.

Отсюда вытекает простое правило проверки формулы (3) на противоречивость: следует проверить каждый элемент множества дизъюнктов формулы на его ложность. Самую высокую эффективность такой проверки дает метод резолюций.

Т.о., преобразование целевой теоремы в противоположную теорему необходимо для получения чистой ПКНФ, нуждающейся в доказательстве своей противоречивости. Вернуться

в) Дизъюнкты Хорна и их назначение.

Дизъюнкты Хорна - это дизъюнкты, которые содержат не более одной позитивной литеры.

Дизъюнкт(ù p Ú ù q Ú ù r Ú S ) эквивалентен импликации

( pÚ qÚ r ) ® S . Общезначимая импликация - это доказанная теорема. Поэтому дизъюнкты Хорна используются в канонической форме целевых теорем в качестве эквивалентов посылок, представляющих собой доказанные теоремы. Эти посылки — доказанные теоремы называются правилами. Правила широко используются при автоматическом доказательстве теорем.

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

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

Второе заключается в том, что вычислительная трудоемкость доказательства целевой теоремы методом резолюций минимальна и не превышает n² , где n - количество литер в канонической форме с учетом повторений.

г) Сущность обратной дедукции.

Основным недостатком прямой дедукции является то, что в ней не существует критериев и управляющих воздействий, которые направляли бы след доказательства к заданной цели и не позволили бы доказательству уйти в сторону от цели. В обратной дедукции эти недостатки устранены.

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

д) Правила доказательства теорем методом резолюций.

Исходным объектом для доказательства является полное множество дизъюнктов, принадлежащих канонической форме целевой теоремы. Обозначим эти множества символом D. Упорядочим D по некоторым критериям, тем самым превратив его в нумерованный список, который обозначим S . Доказательства противоречивости списка S будем производить по следующей рекурсивной схеме.

Берем целевой дизъюнкт, стоящий в голове списка S, и сопоставляем его со всеми последующими, стоящими после него, дизъюнктами. На каждом шаге сопоставления пар дизъюнктов следим за появлением контрарной пары литер Œ A , ù A . Если ее нет, то переходим к следующему дизъюнкту, не производя никаких действий. Если же появляется контрарная пара литер в сопоставляемой паре дизъюнктов, то, вычеркнув ее и породив резольвенту r , запишем ее в конец списка S и присвоим ей номер на единицу больше номера последнего элемента в исходном списке S. Резольвента r дописывается в список при условии, что она не является тавтологией и не поглощается каким-нибудь дизъюнктом из списка S. В этих случаях она просто игнорируется.

После того как первый головной дизъюнкт списка S сопоставлен со всеми последующими дизъюнктами исходного списка S, и вычисленные резольвенты поставлены в хвост списка S , процедура попарного сопоставления элементов повторяется, но теперь уже для нового дизъюнкта, которым становится второй номер дизъюнкта из теперь уже расширенного списка S_p . Рекурсивно повторяются процедуры вычеркивания контрарных пар, порождения резольвент, приписывания резольвент в хвост списка по аналогии с предыдущим циклом. Но первый элемент уже в сопоставлении не участвует, а те резольвенты, которые были порождены в первом цикле, участвуют. Рекурсия с последующими головными элементами продолжается до тех пор, пока текущий список не превращается в пустой дизъюнкт или в набор несопоставимых дизъюнктов. Если появляется пустой дизъюнкт, то теорема доказана, в противном случае - заключение ложно.

От критериев упорядочения списка S зависит эффективность доказательства. Критерии упорядочения списков таковы:

1) первым в S записываются дизъюнкты заключения в любом порядке;

2) во вторую очередь записываются факты в любом порядке;

3) в третью очередь записываются дизъюнкты- правила , но в порядке, соответствующем порядку фактов, т.е. если на первом месте стоит факт a₁ , то правило , включающее факт a₁ в подсписке правил, тоже должно стоять на первом месте.

Примеры доказательства теорем методом резолюций.

Пример 1.

Докажем общезначимость правила 6 , т.е. правила разбора возможных случаев (см. п. 3.2.4). Требуется доказать:

Œ h, h ® ( p Ú q ) , p ® c , q ® c  ® c

Множество дизъюнктов, невыполнимость которого следует установить, таково:

Œ h , ù h Ú pÚ q , ù p Ú c, ù q Ú c , ù c 

Методом резолюций пустой дизъюнкт получим так:

1) ù с - отрицание заключения

2) h - гипотеза

3) ù h Ú p Ú q - гипотеза

4) ù p Ú c - гипотеза

5) ù q Ú c - гипотеза

6) ù p - резольвента для 1 и 4

7) ù q - резольвента для 1 и 5

8) pÚ q - резольвента для 2 и 3

9) q - резольвента для 6 и 8

10) p - резольвента для 7 и 8

11) Л - резольвента для 7 и 9.

Пример 2

Докажем невыполнимость множества.

Œ p Ú q , p Ú r , ù q Ú ù r , ù p 

1) pÚ q

2) pÚ r

3) ù q Ú ù r

4) ù p

5) pÚ ù r - резольвента для 1,3

6) q - резольвента для 1, 4

7) pÚ ù q - резольвента для 2,3

8) r - резольвента для 2,4

9) p - резольвента для 2,5

10) ù r - резольвента для 3,6

11) ù q - резольвента для 3,8

12) Л - резольвента для 4,9. Вернуться