Моделирование рассуждений. Опыт анализа мыслительных актов | страница 47



и ?>2, которые мы перечислили выше. Укажем в специальной табл. 4 классы преобразований F>1, которые можно использовать для устранения различий. Первое различие разделено на два: различие 1 требует добавления выражений в формулу, а различие 1’’ – вычеркивания из формулы лишних выражений.


Таблица 4


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

Покажем работу программы «Логик-теоретик» на несложном примере. Пусть требуется доказать равенство ?>1=?>2, имеющее вид



Применим к ?>1 первое преобразование из F7 справа налево. Выбор F7 определяется различием ?>1 и ?>2. Из ?>1 необходимо убрать лишнее подвыражение С, которого нет в ?>2. После этого получим



Поскольку в ?>1 осталось еще выражение С, которого нет справа, то снова фиксируется различие 1’’ и ищется подходящее преобразование. Таким преобразованием является четвертое из F7. Но для его применения надо сначала использовать преобразование F1 для устранения различия 6. После этого, применяя четвертое преобразование из F7, получаем



Теперь можно применить второе преобразование из F7:



Четвертое преобразование из F7 приводит к окончательному результату



Пример, конечно, не отражает всех особенностей работы программы «Логик-теоретик». Мы несколько упростили задачу. Как видно из таблицы различий, выбор преобразования на каждом шаге далеко не однозначен. В формулах могут существовать одновременно несколько различий, а для ликвидации различия можно использовать несколько преобразований. Всякий вывод, как бы он не был организован, носит переборный характер. И успешность того или иного выбора преобразования не может быть оценена локально, в момент выбора. Поэтому программа вынуждена перебирать варианты, заходить в тупики, проходить циклы прежде, чем она сможет найти правильный путь решения. Повышение эффективности процесса вывода – центральная проблема всех автоматизированных систем дедуктивного вывода.

Исчисление предикатов

Исчисление высказываний не позволяет описывать дедуктивные рассуждения всех типов, в частности силлогистические умозаключения. Оно слишком бедно выразительными средствами.

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