Файл: Методыискусственногоинтеллекта.pdf

74
Гл. 2. Методы автоматизации рассуждений
на основании исследования некоторых элементов класса при отсут- ствии противоречащих примеров.
В отличие от этого, в научной индукции производится анализ и отбор фактов, исключающих случайность обобщения. Умозаключения научной индукции основаны на изучении причинной связи явлений.
Для изучения причинной связи явлений Дж. С. Миль предложил
метод сходства, метод различия, метод сходства–различия. Суще- ствуют и иные методы изучения причинной связи явлений.
Метод сходства — это умозаключение о причине явления, осно- ванное на сравнении двух или более групп факторов, при наличии которых наступает это явление. Если все случаи наблюдаемого явления имеют только один общий фактор, то этот общий фактор и является причиной рассматриваемого явления.
Метод различия — это умозаключение о причине явления, осно- ванное на сравнении случаев, в которых исследуемое явление наступа- ет и не наступает. Если оба случая сходны по всем факторам, кроме одного, и этот фактор присутствует в случае, когда явление наступает,
то он является причиной рассматриваемого явления. Методы индуктив- ных рассуждений особенно востребованы в исследованиях открытых систем.
Абдукция — это способ порождения гипотез, основанный на пере- ходе от частного суждения к частному. В простейшем случае она имеет следующую форму: «из A и B влечет A выводится B». Абдуктив- ная гипотеза B может рассматриваться как возможное объяснение A.
Разумеется этот способ рассуждений также относится к числу правдо- подобных.
Аналогией называют перенос свойств некоторого единичного яв- ления, процесса или предмета на другое единичное явление, процесс или предмет, если между ними замечено сходство их существенных свойств. Различают строгую и нестрогую или простую аналогию.
При строгой аналогии должно быть достоверно установлено, что переносимый признак предмета A с необходимостью связан с призна- ками сходства. Тогда это обстоятельство служит достаточным основа- нием для достоверного переноса этого признака на предмет B.
При простой аналогии зависимость между признаками сходства и переносимым признаком носит правдоподобный характер.
Рассуждения на основе прецедентов (CBR) составляют совокуп- ность методов поиска решения некоторой проблемы при известных решениях подпроблем. В частном случае подпроблема может совпасть с проблемой.
Более точно: задано множество прецедентов (или множество пар) hСЛУЧАЙ, РЕШЕНИЕi, целевая проблема (целевой случай)

2.1. Автоматизация дедуктивных рассуждений
75
ЦЕЛЬ, множество зависимостей внутри прецедентов hСЛУЧАЙ →
РЕШЕНИЕi. Вопрос состоит в следующем: каково же решение целевой проблемы? т. е. какая пара hЦЕЛЬ, РЕШЕНИЕi решает целевую проблему?
Основными задачами в моделировании рассуждений на основе пре- цедентов являются:
— идентификация текущей проблемы;
— поиск подходящего прецедента;
— использование найденного прецедента для решения текущей про- блемы; часто для этого следует выполнить адаптацию старого решения к текущей ситуации.
Некоторые алгоритмы CBR основаны на сравнении прецедентов
(точнее, той их части, которая обозначена нами как СЛУЧАЙ) и целе- вой проблемы и на зависимостях внутри прецедентов. Характеристики задачи могут описываться атрибутами, имеющими численные значения,
или любыми такими атрибутами, на множестве которых задан частич- ный порядок.
Построение такого рода алгоритмов сегодня можно считать важней- шим направлением исследований в области CBR.
Проблемами CBR являются, кроме того, проблема выбора подходя- щего прецедента и адаптация.
Рассуждения на основе аргументации состоят в выдвижении правдоподобных гипотез и их последующем обосновании или опро- вержении. Для этой цели используется множество аргументов, среди которых имеются аргументы «за» и «против».
Более подробное изложение некоторых методов автоматизации рас- суждений будет приведено ниже, и начнем мы с дедуктивных рассуж- дений, а именно, c метода резолюций.
2.1. Автоматизация дедуктивных рассуждений.
Поиск доказательств теорем методом резолюций
Многие интересные и практически важные задачи могут быть сфор- мулированы как задачи доказательства теорем в подходящем логиче- ском исчислении.
Перечислим некоторые из таких задач.
1. Дедуктивные вопросно-ответные системы. В вопросно-ответ- ных системах факты могут быть представлены логическими фор- мулами. Тогда для ответа на некоторый вопрос следует доказать,
что формула, соответствующая ответу, логически выводима из фактов.

76
Гл. 2. Методы автоматизации рассуждений
2. Задача анализа программ. В задаче анализа программ выполне- ние программы можно описать формулой A, а условие завершения работы программы — формулой B. Тогда проверка того, что программа завершит работу, эквивалентна доказательству того,
что формула B следует из формулы A.
3. Задача синтеза программ. Если условие и результат задачи можно представить в виде логических формул, то решение задачи можно рассматривать как логический вывод результата из фор- мул условия. Программа же решения задачи извлекается в этом случае из вывода.
4. Изоморфизм графов. Часто требуется выяснить, изоморфен ли граф подграфу другого графа. Задача может быть сформулирова- на как задача выводимости формулы, представляющий один граф,
из формулы, представляющей другой граф.
Поскольку все перечисленные задачи относятся к трудным вычис- лительным задачам, то через некоторое время после появления вычис- лительных машин, а именно, во второй половине 60-х годов XX в.
наблюдался резкий всплеск интереса к машинному автоматическому поиску доказательств теорем.
На самом деле, поиск универсальной разрешающей процедуры для проверки общезначимости формул был начат еще Лейбницем в XVII в.
В дальнейшем эти попытки возобновили Пеано (на рубеже XX в.)
и Гильберт со своими учениками в 20-х годах XX в.
Эти попытки продолжались до тех пор, пока Черч и Тьюринг в 1936 г. не доказали, что никакой общей разрешающей процедуры для проверки общезначимости формул не существует, иначе говоря, не существует универсального алгоритма, проверяющего общезначимость формул в логике первого порядка.
Это не означает, однако, что общезначимость формулы установить невозможно. Существуют алгоритмы, которые могут установить, что формула общезначима, если она на самом деле общезначима. Если же она не является общезначимой, то эти алгоритмы, вообще говоря,
никогда не закончат свою работу. Это лучшее, что можно ожидать от универсальных алгоритмов поиска доказательства.
Теоретические основы соответствующих компьютерных методов бы- ли заложены в 1930 г. Эрбраном. Первые же практически важные шаги на пути создания программ автоматического доказательства тео- рем были сделаны после основополагающих работ С. Ю. Маслова [25]
об обратном методе установления выводимости в классическом ис- числении предикатов и Дж. А. Робинсона [26] о методе резолюций,
выполненных ими независимо в 1964 и 1965 годах соответственно.

2.1. Автоматизация дедуктивных рассуждений
77
2.1.1. Скулемовская стандартная форма. При поиске доказа- тельства методом резолюций используются так называемые скулемов- ские стандартные формы формул исчисления предикатов первого по- рядка.
При приведении формулы к скулемовской стандартной форме ис- пользуются следующие соображения:
1. Формула логики первого порядка может быть приведена к пре-
нексной нормальной форме, в которой все кванторы содержатся в префиксе (т. е. ни одному квантору не предшествует предикат- ный символ).
2. Матрица (т. е. часть формулы, следующая за префиксом и не содержащая кванторов) может быть сведена к коньюктивной
нормальной форме.
3. В формуле можно элиминировать кванторы существования с по- мощью скулемовских функций.
Рассмотрим вначале метод приведения формулы к пренексной нор- мальной форме [27]. Для этого рассмотрим основные законы эквива- лентности в логике первого порядка. Здесь мы полагаем, что x и y являются свободными переменными в формулах A и B, соответственно:
1
◦
. – (∃x)A(x) ∨ (∃x)B(x) = ∃x((A(x) ∨ B(x));
2
◦
. ¬(∀x)A(x) = ∃x(¬A(x));
3
◦
. ¬(∃x)A(x) = (∀x)(¬A(x));
4
◦
. F ↔ G = (F → G) ∧ (G → F );
5
◦
. (∀x)A(x) ∧ (∀x)B(x) = ∀x(A(x) ∧ B(x));
6
◦
. F → G = ¬F ∨ G.
Имеется и ряд других эквивалентностей, которые будут использо- ваться по мере необходимости.
Здесь уместно заметить, что квантор всеобщности ∀ и квантор существования ∃ нельзя проносить через дизъюнкцию и конъюнкцию соответственно, т. е.
(∀x)A(x) ∨ (∀x)B(x) 6= ∀x(A(x) ∨ B(x)),
(∃x)A(x) ∧ (∃x)B(x) 6= ∃x((A(x) ∧ B(x)).
В таких случаях надо вспоминать, что связанная переменная — лишь место для подстановки какой угодно переменной и, следовательно,
каждую связанную переменную можно переименовать. Например, фор- мулу
(∀x)A(x) ∨ (∀x)B(x)
можно преобразовать в формулу (∀x)A(x) ∨ (∀z)B(z), где z не встре- чается в A(x). Тогда
(∀x)A(x) ∨ (∀z)B(z) = (∀x)(∀z)(A(x) ∨ B(z)).

78
Гл. 2. Методы автоматизации рассуждений
Аналогичным образом преобразуется и формула
(∃x)A(x) ∧ (∃z)B(z) = (∃x)(∃z)(A(x) ∧ B(z)).
Далее формулу следует привести к следующему виду:
(Q
1
x
1
) ... (Q
n x
n
)(M ),
где каждое Q
i x
i
(i = 1, 2, ..., n) есть или (∀x i
) или (∃x i
), а M есть формула, не содержащая кванторов. Такой вид и будет называться пренексной нормальной формой.
Тогда (Q
1
x
1
) ... (Q
n x
n
) называют префиксом, а M — матрицей формулы.
Опишем теперь кратко алгоритм приведения формул к предварен- ной нормальной форме [27]:
1. Если в формуле присутствуют логические связки ↔ и →, то прим´еним к ней законы
F ↔ G = (F → G) ∧ (G → F ),
F → G = ¬F ∨ G
для исключения этих связок.
2. Если перед формулой имеется знак отрицания, то используем за- коны
¬(¬F ) = F ,
¬(F ∨ G) = ¬F ∧ ¬G,
¬(F ∧ G) = ¬F ∨ ¬G
и законы
¬(∀x)A(x) = ∃(x¬A(x)),
¬(∃x)A(x) = (∀x)(¬A(x)),
для того, чтобы пронести знак отрицания внутрь формулы.
3. Если необходимо, переименовываем связанные переменные.
4. Выносим кванторы в начало формулы, для чего используем за- коны
(∀x)A(x) ∧ (∀x)B(x) = ∀x(A(x) ∧ B(x)),
(∃x)A(x) ∨ (∃x)B(x) = ∃x((A(x) ∨ B(x)),
(Qx)A(x) ∨ G = (Qx)(A(x) ∨ G),
(Qx)A(x) ∧ G = (Qx)(A(x) ∧ G),
(Q
1
x)A(x) ∨ (Q
2
x)B(x) = (Q
1
x)(Q
2
y)((A(x) ∨ B(y)),
(Q
1
x)A(x) ∧ (Q
2
x)B(x) = (Q
1
x)(Q
2
y)((A(x) ∧ B(y)).

2.1. Автоматизация дедуктивных рассуждений
79
Далее следует M — матрицу формулы — привести к конъюнктивной нормальной форме.
Для этого введем следующие определения.
Определение 2.1.1. Литерой будем называть атомарную формулу или ее отрицание.
Определение 2.1.2. Формула F находится в конъюнктивной нор- мальной форме тогда и только тогда, когда F имеет вид n > 1, а каждая
F
1
, F
2
, ..., F
n есть дизъюнкция литер
F
1
∧ F
2
∧ ... ∧ F
n
Приведем схематическое описание процедуры преобразования к конъюнктивной нормальной форме (впрочем, следует заметить, что эта же схема годится и для дизъюнктивной нормальной формы):
1. Элиминируем логические связки → и ↔, применяя эквивалент- ности
F ↔ G = (F → G) ∧ (G → F ),
F → G = ¬F ∨ G.
2. Проносим знак отрицания к атомам, используя (возможно,
несколько раз) законы
¬(¬F ) = F ,
¬(F ∨ G) = ¬F ∧ ¬G,
¬(F ∧ G) = ¬F ∨ ¬G.
3. Используем (возможно, несколько раз) законы
F ∨ (G ∧ H) = (F ∨ G) ∧ (F ∨ H),
F ∧ (G ∨ H) = (F ∧ G) ∨ (F ∧ H)
для получения нормальной формы.
После выполнения соответствующих процедур для приведения фор- мулы к скулемовской нормальной форме осталось элиминировать кван- торы существования. Это выполняется следующим образом: пусть формула имеет вид (Q
1
x
1
) ... (Q
n x
n
)(M ), где M есть конъюнктивная нормальная форма, и пусть некоторое Q
i есть квантор существования в префиксе (Q
1
x
1
) ... (Q
n x
n
)(M ).
Если в указанном префиксе левее Q
i нет никакого квантора все- общности, выбирается новая константа c, отличная от всех иных кон- стант, входящих в M , и все x i
в M заменяются на c. Если же левее

80
Гл. 2. Методы автоматизации рассуждений
Q
i встречаются кванторы всеобщности Q
α
, ..., Q
χ
, выбирается новый m-местный функциональный символ f , отличный от всех иных функ- циональных символов в M , то все x i
в M заменяются на f(x
α
, ..., x
χ
) и
(Q
i x
i
) вычеркивается из префикса. Затем этот процесс применяется ко всем кванторам существования в префиксе. Последняя из полученных таким образом формул и есть скулемовская нормальная форма. Кон- станты и функции, используемые для замены переменных, связанных кванторами существования, называются скулемовскими функциями.
Введем понятие дизъюнкта.
Определение 2.1.3. Дизъюнкция литер называется дизъюнктом.
Далее там, где это будет удобно, будем рассматривать как синоним дизъюнкта множество литер.
Определение 2.1.4. Если A — атомарная формула, то две литеры
A и ¬A называют контрарными, а множество {A, ¬A} — контрарной парой. Заметим, что если дизъюнкт содержит контрарную пару, то он является тавтологией. Если дизъюнкт не содержит литер, то он называется пустым дизъюнктом, если он содержит одну литеру, то называется однолитерным дизъюнктом, а если содержит k литер —
k-литерным дизъюнктом. Так как пустой дизъюнкт не содержит литер,
которые могли бы быть истинны, то он всегда ложен. Пустой дизъюнкт обозначается .
Каждое множество дизъюнктов S будем считать конъюнкцией
всех дизъюнктов из
S, где каждая переменная считается связанной квантором всеобщности. Тогда скулемовская стандартная форма может быть представлена множеством дизъюнктов.
Справедлива следующая
Теорема 2.1.1. Пусть S — множество дизъюнктов, представ-
ляющих скулемовскую стандартную форму формулы
F . Тогда F
невыполнима в том и только в том случае, когда
S противоречиво.
Д о к а з а т е л ь с т в о теоремы мы опустим.
Далее для множеств дизъюнктов будут использованы термины невыполнимо/выполнимо вместо противоречиво/непротиворечиво.
2.1.2. Метод резолюций для исчисления высказываний. Ос- новная идея метода резолюций состоит в том, чтобы проверить, со- держит ли множество S пустой дизъюнкт . Если S содержит пустой дизъюнкт, то, как следует из предыдущего параграфа, S невыполнимо.
Если S не содержит , то проверяется: может ли быть получен из S? Метод резолюций можно рассматривать как специальное правило вывода, используемое для порождения из S новых дизъюнктов. Это

2.1. Автоматизация дедуктивных рассуждений
81
правило вывода таково:
в том случае, если для любых двух дизъюнктов
C
1
и
C
2
суще-
ствует литера
L
1
в
C
1
, которая контрарна литере L
2
в
C
2
, то
вычеркнув
L
1
и
L
2
из
C
1
и
C
2
соответственно можно построить
дизъюнкцию оставшихся дизъюнктов, которая будет являться
следствием
C
1
и
C
2
. Эта последняя дизъюнкция называется ре-
зольвентой.
Корректность этого правила вывода устанавливает следующая
Теорема 2.1.2. Пусть даны два дизъюнкта C
1
и
C
2
. Тогда ре-
зольвента С дизъюнктов
C
1
и
C
2
есть логическое следствие
C
1
и
C
2.
Д о к а з а т е л ь с т в о. Пусть
C
1
= L ∨ C
a
,
C
2
= ¬L ∨ C
b
,
C = C
a
∨ C
b
,
где C
a и C
b
— дизъюнкции литер. Предположим, что C
1
и C
2
истинны в некоторой интерпретации I. Очевидно, либо L, либо ¬L ложно в I.
Пусть, например, L ложно в I. Тогда C
a должен быть истинен в I
(иначе предположение об истинности C
1
неверно). Таким образом,
резольвента, т. е.
C
a
∨ C
b истинна в I. Аналогично можно показать, что если ¬L ложно в I, то
C
b должен быть истинен в I. Следовательно,
C
a
∨ C
b истинна в I, что требовалось доказать.
Пример 2.1.1. Рассмотрим множество дизъюнктов
¬Q ∨ R,
Q ∨ P ,
тогда резольвента этих двух дизъюнктов есть
P ∨ R.