Синтез блок-схемы. 
Символический искусственный интеллект: математические основы представления знаний

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

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

Рассмотрим такой пример: синтез программы, которая вычисляет знак числа:

у := if х>0 then 1 else -1 end if (5.1).

Обозначим через Р предикат, который проверяет, что его аргумент больше нуля: Р (х) := х > 0, а предикат Q (x, у) — постусловие, которое связывает входные данные х с выходными данными у.

Тогда исходная аксиоматика, т. е. спецификация задачи, имеет следующий вид:

Преобразуем в дизъюнкты и проведем вывод методом резолюций.

Исходные дизъюнкты:

• 1) ^Р (х) v Q (x, 1);
• 2) Р (х) v Q (x, -1).

Вопрос, записанный с участием предиката ANS:

3) -.?>(*, у) v ANS (y).

Вывод:

• А)^Р (х) vANS (l) 1,3;
• 5) ад vANS (-l) 2,3;
• 6) ANS (l) v ANS (-l) 4,5.

Проводим обычное резольвирование. Резольвируем дизъюнкты 1 и 3 но предикату Q, получает —iQ (x, у) v ЛМ9(1). Дальше резольвируем 2 и 3 по предикату Q еще раз и получаем Р (х) v ЛМ5(-1). Резольвируем два последних дизъюнкта по предикату Р. В результате получаем ANS () v v ANS (-1). Доказано, что ответ существует (рис. 5.2).

Рис. 5.2. Дерево доказательства.

Сверху написаны исходные предложения, ниже, в узлах дерева, — результаты их резольвирования, еще ниже — результаты последнего резольвирования.

Это дерево доказательства, т. е. запись логического вывода. Однако из этого дерева легко извлекается реальная блок-схема.

Первый шаг алгоритма извлечения блок схемы из доказательства состоит в том, что мы навешиваем на дуги дерева доказательства подстановки и отрицание тех литералов, по которым проводилось резольвирование (рис. 5.3).

Рис. 53. Дерево доказательства с дополнительной информацией.

На втором шаге мы убираем лишнюю информацию из этого дерева, т. е. удаляем все узлы, в которых пет предиката ANS. Это два узла находятся на самом верхнем уровне дерева. После этого переворачиваем дерево корнем вверх (рис. 5.4).

Рис. 5.4. Дерево доказательства с удаленными ненужными узлами.

Третий шаг — убираем надписи предикатов во всех узлах, а также надписи предикатов на тех дугах, которые являются единственными исходящими. Результат представлен на рис. 5.5. Для наглядности по правилам UMD стартовый узел закрашен, а заключительные узлы выглядят как «бычий глаз».^[1]

Рис. 5.5. Синтезированная блок-схема.

Эта блок-схема решает задачу (5.1), и она получается из доказательства автоматически.

Формализуем использованный в примере алгоритм.

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

Вход: дерево вывода Т₀ (в узлах — предложения).

Выход: схема программы Т (дерево решений).

Если имеется дерево Т₀, применим к нему следующие шаги преобразования.

Шаг 1: поместить на дуги отрицание литерала, по которому проводилась резолюция вместе с унификатором.

Шаг 2: удалить все узлы (и инцидентные им дуги), где нет предиката ANS.

Шаг 3: перевернуть дерево корнем вверх и удалить предложения из узлов.

Шаг 4: удалить литералы на дугах, выходящих из узлов с одним выходом. При этом унификатор остается (получим дерево 7).

• [1] Новиков Ф. А., Иванов Д. 10. Моделирование на UML. Теория, практика, видеокурс.