Продолжим обсуждение работы системы, структура которой показана на рис. 18. Возможны два режима работы системы: режим пополнения базы фактов и режим доказательства теоремы. В первом случае происходит добавление в базу фактов всех тех фактов, которые с помощью силлогистического вывода получаются из вновь введенного факта, и всех фактов, ранее хранившихся в базе фактов. Во втором случае формулируется теорема в виде вопроса о возможности вывода факта, поступившего на вход системы, из фактов, хранящихся в базе фактов. В процессе вывода блок формирования совместимых посылок выбирает из базы фактов пары посылок, которые образуют одну из четырех фигур силлогизма, т.е. посылок, сцепленных между собой общим классом сущностей М.
После нахождения такой пары она передается в блок формирования заключения. В этом блоке проверяется возможность вывода, т.е. возможность того, что пара типов посылок в данной фигуре силлогизма образует правильный модус. Если правильный модус не образуется, то вырабатывается требование на поиск новой пары посылок. Если же вывод возможен, то его результат сравнивается с высказыванием, являющимся целью доказательства теоремы. Если полученное заключение есть искомое высказывание, то процесс доказательства обрывается и результат, говорящий о том, что теорема верна, выдается из системы. Если этого не произошло, то полученное заключение добавляется в базу фактов и процесс поиска доказательства продолжается.
В рассмотренной процедуре возникает проблема остановки. Если нужный факт не выводится из той системы посылок, которая имеется в базе фактов, то как это узнать? Единственный возможный ответ связан с полным перебором всех сочетаний посылок, дающих фигуры силлогизма. Это же касается и случая прекращения процесса пополнения базы фактов после введения нового факта в систему.
Суммируя все сказанное, необходимо отметить, что, несмотря на внешнюю простоту процедуры вывода в силлогистике, в ней, как в капле воды, отражаются все те трудности, которые связаны с поиском вывода. Прежде всего это трудности понимания поступающих в систему сообщений, истолкования их в терминах, понятных на уровне внутреннего языка (в нашем случае это необходимость в процедурах нормализации сообщений). Затем это ряд трудностей, вызываемых процедурами проверки поступающего сообщения на согласованность содержащейся в нем информации с той информацией, которая ранее хранилась в памяти системы. Это трудности поиска, не опирающегося на какую-то цель, или при известной цели (в случае доказательства теоремы) не опирающегося на какие-либо соображения о путях движения по дереву вывода. Наконец, это трудности, связанные с прекращением процедур вывода и формированием отрицательного ответа на поставленный перед системой вопрос о выводимости.
