12.9. Проблемы и будущие разработки
В области автоматического доказательства теорем отмечается значительный прогресс. Однако, несмотря на это, программы доказательства теорем, основанные на резолюциях, склонны порождать слишком много предложений и исследовать слишком много бесполезных путей. Легко указать задачи, для решения которых не хватает памяти и быстродействия существующих в настоящее время машин. Это натолкнуло на мысль применить для определенной области задач специфические методы (Хоуде, 1970) или использовать более ограничительные, хотя и не обладающие полнотой, правила вывода (Бледсоу, Бойер и Хеннеман, 1972). Последний подход напоминает известные методы (также не обладающие полнотой), применявшиеся в FDS, GPS и других аналогичных программах. Третья альтернатива, предложенная Робинсоном (1969, 1970, 1971), заключается в использовании исчисления предикатов высоких порядков, что позволяет обращаться со сложными отношениями более прямым путем, чем это допускают часто неуклюжие представления, ограниченные конъюнкциями дизъюнкций. С точки зрения программирования это меняет задачу, и вместо простых операций с большим числом высказываний выполняются сложные операции с небольшим их числом. В близком подходе Петржиковского (1973) принцип резолюции распространен на исчисление; это позволяет использовать переменные функции и имена предикатов.
Был предложен и совершенно отличный от упомянутых, нематематический метод. В принципе не плохо бы приспособить человека
для утонченных подсказок машине, доказывающей теоремы. Это вызвано тем, что обычно устройства доказательства теорем оказываются не в состоянии решить задачу из-за того, что слишком много „усилий» тратится на проведение определенной линии доказательства уже после того, как человеку „стало бы очевидна» невозможность найти решение на этом пути. Время от времени утверждается, что люди способны чувствовать обещающий подход к решению задачи, но пасуют при необходимости механически применять на каждом шаге правила вывода. Если это так, то комбинация человека и машины должна привести к системе с известным свойством: целое больше, чем сумма его частей. В ряде проектов делались попытки использовать эту идею, однако без большого успеха (Аллен и Лакхэм, 1970; Гард, Оглсби, Беннетт и Сеттл, 1969; Грин, 1970). Такие проекты уводят нас от области искусственного интеллекта в еще более неопределенную область человеко-машинного интеллекта. Защитники человеко-машинных систем должны ответить на следующие вопросы. Совершенно неясно, действительно ли (или при каких обстоятельствах) человек способен предчувствовать, что определенная линия рассуждения приведет к успеху. Гард и др. (1969), выполнившие, вероятно, наиболее обширные исследования в этой области, отмечают, что наблюдать за работой автоматического устройства доказательства теорем — это почти то же, что проникнуть в мысли сильного математика с нечеловеческим мышлением. Это можно увидеть, следя за ходом доказательств (безусловно, верных), полученных программой доказательства теорем. Тогда для построения человеко-машинной системы нужен язык, на котором могут общаться друг с другом эти две компоненты. Сомнительно, чтобы для этого был достаточен какой-нибудь общепринятый язык программирования, известный в настоящее время, хотя PLANNER и 
открывают интересные возможности. Наконец, наш собственный ограниченный опыт указывает на то, что инженерно-человеческий аспект такого взаимодействия становится весьма важным. В конце концов даже шум, производимый телетайпом, при решении вместе с машиной сложной задачи доказательства теорем может создавать серьезные трудности. Кроме того, необходимая психомоторная концентрация при наборе сообщений, которые приходится посылать вычислительной машине, мешает человеку следить за смыслом этих сообщений. Вовсе отсутствуют исследования, позволяющие оценить „человеческие факторы" в доказательстве теорем или вообще в математике.
