Для дальнейшего повышения эффективности поиска целесообразно использовать более структурированное представление, описание моделей мира, например, па основе отделения существенной информации от несущественной и построения на этой основе иерархии моделей мира. Так возникла система ABSTRIPS. Эта система представляет собой модификацию решателя STRIPS, использующую иерархию описаний мира задач.
Используемый в ABSTRIPS метод иерархического планирования хотя и увеличил эффективность поиска по сравнению с системой STRIPS, однако, не основываясь па достаточно полном обобщении, все еще желал много лучшего. В этой системе обобщение операторов и моделей мира производилось путем исключения деталей, в то время как человеку в его мыслительной деятельности свойственно обобщать путем укрупнения, свертывания как моделей, так и операторов (см. § 4.4). Только такое обобщение могло бы позволить значительно повысить эффективность поиска.
Опыт разработок систем STRIPS и ABSTRIPS показал, что автоматическое доказательство теорем на основе метода резолюций недостаточно эффективно по причине неструктурированности знаний. Любая теорема в методе резолюций представляется отдельным утверждением без каких-либо ссылок на другие вспомогательные теоремы, которые можно было бы использовать для доказательства данной теоремы. В действительности каждая теорема должна по возможности задаваться как фрейм, содержащий в себе всю полезную информацию, необходимую для направленного поиска доказательства данной теоремы. Другими словами, теорему желательно задавать в процедуральной форме, указывающей, что и в какой последовательности необходимо сделать предварительно, прежде чем доказать данную теорему.
Эта идея легла в основу разработок современных процедуральных языков высокого уровня, таких как PLANNER, QA4, QLISP, CONNIVER и др., ориентированных на машинное решение интеллектуальных задач. В них удобно реализуется представление знаний с помощью специального вида базы данных и процедур. Эти языки ориентируются на автоматическое доказательство теорем, автоматическую проверку и синтез машинных программ, па планирование деятельности робота и многое другое. Построение решателей на базе подобных языков представляется перспективным направлением.
В оставшейся части главы мы рассмотрим более подробно вышеупомянутые зарубежные решатели в трех аспектах: представление знаний, поиск решений и обучение.
Исследование проблемы автоматизации доказательств началось почти одновременно в Советском Союзе и США. Уже в первой половине 60-х годов в этих странах, независимо друг от друга* были разработаны основы двух методов автоматических доказательств: обратный метод С. Ю. Маслова [1964, 1968J — Советский Союз и принцип резолюций Робинсона [1965] — США'.
В Ленинградском отделении Математического института (ЛОМИ) АН СССР группой логиков в 1965 г. было разработана несколько версии алгоритма машинного поиска естественного логического вывода в исчислении высказываний (АЛПЕВ) [Н.А. Ша-пин, Г. В. Давыдов и др., 1965]. В том же институте на основе обратного метода в 1969 г. был разработан машинный алгоритм исчисления предикатов первого порядка [Г. В. Давыдов* С. Ю. Маслов и др., 1969].
Разработка версий систем АЛПЕВ-ЛОМИ и алгоритма исчисления предикатов носила поисковый, научно-исследовательский характер и показала принципиальную возможность машинных доказательств на основе секвенциальных исчислений.
Первым отечественным решателем, по-видимому, следует считать систему программирования ПРИЗ (пакет прикладных инженерных задач), созданную таллиннским коллективом научных сотрудников под руководством проф. Э. X. Тыугу. Начало разработки системы следует отнести к 1970—1971 гг., затем она несколько раз усовершенствовалась вплоть до 1976 г. [Э. X. Тыугу, 1970, 1971; М. А. Мянписалу, Э. X. Тыугу, 1974; Э. X. Тыугу, М. Упг„ 1976; М. И. Кахро, М. А. Мянписалу, 10. П. Саан, Э. X. Тыугу, 1976].
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.