«Логик-теоретик»

Так была названа программа для ЭВМ, созданная в середине шестидесятых годов американским кибернетиком А. Ньюэллом в содружестве с психологом Г. Саймоном. Она была предназначена для доказательства теорем в исчислении высказываний, т.е. для поиска обоснования тождественной истинности некоторых утверждений. Для того чтобы перейти к описанию программы «Логик-теоретик», введем предварительно понятие о равенстве двух выражений исчисления высказываний. Будем говорить, что выражения ?₁ и ?₂ равны между собой, и записывать этот факт обычным образом ?₁=?₂, если на всех возможных наборах интерпретации истинности входящих в них элементарных высказываний истинность ?₁ и ?₂ одинакова.

Появление знака равенства, которого не было в исчислении высказываний, не должно нас смущать. Его легко можно исключить из рассмотрения, введя формулу ((?₁&?₂)(?₁&?₂)). Читатели могут проверить, что эта формула будет истинной только в том случае, когда оценки истинности ?₁ и ?₂ одинаковы. Тогда утверждение, что ?₁=?₂, становится эквивалентным утверждению, что формула ((?₁&?₂)(?₁&?₂)) является истинной.

«Логик-теоретик» должен был доказывать справедливость утверждений вида ?₁=?₂ для различных ?₁ и ?₂. Однако авторы «Логика-теоретика» не пошли по прямому пути. Не стали строить таблицы для ?₁ и ?₂ и проверять совпадение истинности ?₁ и ?₂ на всех возможных интерпретациях истинности их аргументов. Ведь с ростом числа аргументов n число строк в этих таблицах растет как 2ⁿ. А. Ньюэлл и Г. Саймон пошли по пути приближения процедуры доказательства к тому, как это делают люди.

В основу процесса доказательства они положили идею ликвидации различий в формульной записи ?₁ и ?₂. Авторы программы составили перечень из шести различий.

1. В ?₁ и ?₂ различное число членов в формулах. Например, ?₁=??, а ?₂=??[6].

2. В ?₁ и ?₂ имеется различие в основной связке (т.е. в связке, которая выполняется последней). Например, ?₁=(??)(), а ?₂=(?)?.

3. Перед всем выражением для ?₁(?₂) стоит знак отрицания, а перед ?₂(?₁) его нет. Например, ?₁=(??), а ?₂=??.

4. Аналогичное различие, но оно касается не всего выражения для ?_i (i=1,2), а некоторого его подвыражения.

5. Скобки в ?₁ расставлены не так, как в ?₂. Например, ?₁=?(??), а ?₂=(??)?.

6. Записи для ?₁ и ?₂ отличаются порядком следования подвыражений. Например, ?₁=(??)?, а ?₂=?(??).

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

В преобразованиях использованы большие латинские буквы, которые могут соответствовать любым подвыражениям формул ?₁ и ?₂. Стрелки и показывают направление преобразований. (Знак есть по сути знак .)

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

Таблица 4

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

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

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

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

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

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

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

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

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

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

Под предикатом будем понимать некоторую связь, заданную на наборе из констант или переменных, например утверждение «? больше ?». Если семантика ? и ? не задана, то о предикате сказать особенно нечего. Пожалуй, только то, что он задает двуместное отношение, семантика которого такова, что оно является антирефлексивным (неверно, что «? больше ?»), асимметричным и транзитивным. Но при задании семантики (т.е. областей определения переменных ? и ?) о предикате можно будет сказать существенно больше. Если ? и ? – площади городов соответственно в СССР и Японии, то при задании списков городов и означивании переменных константами мы получим отношение между двумя высказываниями типа «Площадь Вологды больше площади Токио» или «Площадь Ленинграда больше площади Нары». После этого становится возможным говорить об истинности или ложности предиката. Для нашего примера первое означивание дает ложное значение предиката, а второе – истинное. Иногда для утверждения об истинности или ложности предиката можно обойтись и без означивания. Например, если областью определения х являются целые положительные числа, то предикат «х больше ?5» будет тождественно истинен.

В исчислении предикатов используются те же операции, что и в исчислении высказываний. С их помощью образуются предикатные формулы. Будем обозначать предикаты большими латинскими буквами. Примерами предикатных формул могут служить Р(х,у)&Q(a,b) или P(?)P(z,l).

В исчислении предикатов используются два квантора: квантор общности и квантор существования. Первый обозначается как , а запись xP(x) эквивалентна утверждению «Для всех х из области его определения имеет место Р(х)». Второй квантор обозначается как , а запись хР(х) эквивалентна утверждению «Найдется по крайней мере один х* в области определения х, такой, что истинен Р(х*)». Переменные, находящиеся в сфере действия кванторов, называются связанными, остальные переменные – свободными.

Вспомним И.А. Крылова: «А вы, друзья, как ни садитесь, все ж в музыканты не годитесь!». Обозначим через Р(х,у) предикат, который связывает между собой способ рассаживания участников квартета и качество исполняемой ими музыки. Предикат Р(х,у) становится истинным лишь тогда, когда найдено такое взаимное расположение зверей в квартете, что качество музыки позволяет назвать исполнителей музыкантами. При этих условиях цитате из басни «Квартет» соответствует формула xP(x,у).

А вот Ф. Тютчев: «Бывают роковые дни лютейшего телесного недуга и страшных нравственных тревог…». Если Q(u,v) есть предикат, в котором переменная u определена на множестве дней, а переменная v на области настроений, связанных с «телесным недугом» и «страшными нравственными тревогами», то в исчислении предикатов началу стихотворения Тютчева будет соответствовать формула uQ(u,v).

Отметим, что имеют место следующие соотношения:

Справедливость их вытекает из смысла кванторов. Они позволяют любую формулу в исчислении предикатов представить в виде предваренной нормальной формы (ПНФ). В ней сначала выписываются все кванторы, а затем предикатные выражения. Например, формула

записана в ПНФ.

Введение кванторов и , а также их отрицаний наводит на мысль о связи исчисления предикатов и силлогистики Аристотеля. Вспомним еще раз смысл кванторов, использованных в силлогистике: Asp – «Всякое s есть р»; Esp – «Ни одно s не есть р», Isp – «Некоторые s есть р» и Osp – «Некоторые s не есть р». Представляется вполне справедливым заменить эти выражения силлогистики следующими четырьмя формулами исчисления предикатов:

На первый взгляд такая замена вполне законна. Но для того, чтобы убедиться в этом, необходимо показать, что в исчислении предикатов могут быть выведены все модусы силлогистики Аристотеля.

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

Смысл их очевиден. Первая аксиома говорит о том, что если Р(х) истинен для любых х, то и для некоторого у из того же универсума истинность предиката должна сохраняться. Вторая аксиома говорит о том, что если найдется такое у, что Р(у) будет истинным, то верно, что существует х, для которого Р(х) истинно.

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

1. Пусть F₁ и F₂ – две формулы исчисления предикатов. И пусть в F₁ переменная х не входит, а в F₂ входит в качестве свободной переменной. Пусть, наконец, формула F₁F₂ является выводимой. Тогда выводима и формула F₁xF₂.

2. Если х содержится в качестве свободной переменной в F₁ и не содержится в таком виде в F₂ и если F₁F₂ – выводимая формула, то xF₁F₂ также является выводимой.

3. Если F – выводимая формула и в F есть кванторы общности и существования, то любая из связанных ими переменных может быть заменена на другую связанную переменную одновременно во всех областях действий квантора и в самом кванторе. Полученная после этого формула также является выводимой.

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

Вернемся теперь к попытке вложения силлогистических утверждений в исчисление предикатов. Исследование выводимости 24 модусов, верных в силлогистике Аристотеля, в исчислении предикатов привело к следующему результату. Если предполагать, что все классы сущностей непусты, т.е. рассуждения не касаются мыслимых сущностей (например, драконов или русалок), то приведенная выше замена силлогистических выражений выражениями логики предикатов будет полностью справедлива. Другими словами, при непустых классах сущностей все модусы силлогистики Аристотеля выводятся в исчислении предикатов.

Иная ситуация возникает при допущении пустых классов сущностей. В исчислении предикатов предикаты с пустыми областями для аргументов ведут себя совсем не так, как такие же предикаты с непустыми областями. В этих условиях оказываются невыводимыми все модусы силлогистики, в которых вывод носит частный характер, а обе посылки носят общий характер. Например, оказываются невыводимыми модусы AAI и ЕАО первой фигуры:

Хотелось бы обратить внимание читателей на только что полученный результат моделирования. Даже в области дедуктивных рассуждений, дающих всегда достоверные результаты, характер человеческих рассуждений может быть различным. И он не обязан совпадать (как это показывает случай с силлогистикой) с теми схемами рассуждений, которые демонстрирует исчисление предикатов.

Общая схема вывода

Опишем общую схему выводов, лежащую в основе большого количества моделей человеческих достоверных рассуждений. Она приведена на рис. 19. Обратим сначала внимание на рис. 19, а. На нем показано некоторое дерево вывода. Вершинам этого дерева соответствуют определенные утверждения F_i, а дуги определяют порядок получения новых утверждений. Те дуги, которые сходятся в зачерненные точки, образуют конъюнктивные условия вывода, а те дуги, которые между собой соединены «дужкой», образуют дизъюнктивные условия вывода. Например, получение утверждения F₉ возможно двумя путями. Если доказаны утверждения F₂ и F₃, то F₇ следует из их доказанности, F₆ из доказанности F₂ и F₉ из доказанности F₆ и F₇. Другой путь доказательства F₉ вытекает из априорной доказанности F₃ или F₄. Любого из этих фактов достаточно для вывода F₈, который обеспечивает выводимость F₉.

Рис. 19.

Дерево вывода с такими условиями переходов от вершины к вершине носит название И-ИЛИ дерева. В И-ИЛИ дереве ориентация дуг показывает направление вывода. Естественное разбиение вершин дерева по ярусам отражает глубину вывода (число шагов, необходимых для получения утверждений данного яруса). Первый ярус дерева образуют вершины (на рис. 19, а это вершины F₁, F₂, F₃, F₄), играющие роль аксиом или утверждений, истинность которых задается извне.

Схема вывода не обязательно описывается в виде дерева. Она может иметь вид произвольной сети, ориентированной, неориентированной или частично ориентированной. На рис. 19, б показан пример неориентированной сети. Такая сеть (наличие или отсутствие ориентации не играет здесь роли) называется И-ИЛИ сетью. Процесс вывода на И-ИЛИ сети протекает следующим образом. Пусть мы хотим доказать утверждение ?₆ (на рис. 19, б этому соответствует целевая вершина). В качестве априорно доказанного задано утверждение ?₁ (ему соответствует начальная вершина, которая на рис. 19, б заштрихована). Как из ?₁ можно получить ?₆? Если считать, что все связи допускают ориентацию в нужную сторону, то из ?₁ можно получить ?₃, затем ?₅ и, наконец, ?₆. Но этот путь нам удалось отыскать потому, что сеть, показанную на рис. 19, б, мы видим «с птичьего полета». Лабиринт поиска лежит в виде чертежа перед нами. Именно это позволяет нам не делать лишних попыток, не двигаться в ненужную сторону, а идти кратчайшим путем к цели.

Подобная ситуация приятна, но редко встречается в действительности. При решении любой задачи, даже если заранее известен ее ответ, к которому надо стремиться (для школьника эта ситуация с подглядыванием в ответ до решения задачи весьма типична), мы не видим перед собой полного лабиринта возможностей. Мы пытаемся построить этот лабиринт, видя лишь начальные «площадки лабиринта» и не зная, что лежит между ними и «целевыми площадками». В нашем примере мы стоим на начальной площадке, в вершине ?₁, и не знаем, куда идти. Мы делаем попытку перейти в ?₂ (т.е. вывести утверждение), но видим, что этого нельзя сделать. Тогда мы движемся в сторону утверждения ?₃ и обнаруживаем, что его доказательство возможно. Теперь в нашем распоряжении две площадки лабиринта: ?₁ и ?₃. Из ?₃ можно двигаться в четырех направлениях. Одно из них, ведущее назад к ?₁, интереса не представляет. Попытка продвинуться к ?₂ и ?₅ оказывается успешной. Возникает новый фронт достигнутых площадок (доказанных утверждений). Теперь его образуют ?₂, ?₃ и ?₅. Площадка ?₁ исключается из активного фронта, так как использованы все связи этой площадки с другими площадками лабиринта. На следующем шаге достигаются площадки ?₄ и ?₆. Наличие среди доказанных выражений целевого ?₆ позволяет завершить процесс доказательства. После этого можно произвести «чистку», в результате которой останется лишь тот путь, который кратчайшим образом приводит от начального утверждения ?₁ к целевому ?₆.

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

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

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

Несколько иной разновидностью схем вывода являются так называемые альтернативные деревья или альтернативные сети. В этих схемах выбор дальнейшего пути движения зависит от того, достигнут или не достигнут вывод некоторого выражения. Другими словами, попытки продвижения по лабиринту, которые мы демонстрировали на методе прямой волны при удачах и неудачах, могут влиять на стратегию дальнейшего движения. Такие схемы вывода мы более подробно рассмотрим в пятой главе. Здесь же лишь проиллюстрируем рассуждение такого типа на примере.

В знаменитом рассказе «Убийство на улице Морг» Эдгара По сыщик-любитель Огюст Дюпен помещает в газете объявление о находке орангутанга, который, по слухам, принадлежит матросу мальтийского корабля. На вопрос о причинах такого объявления Огюст Дюпен отвечает следующим образом: