Cтраница 1
Система доказательства теорем чарует и влечет. [1]
Система доказательства теорем может являться частью разумной системы, но она совершенно очевидно не представляет собой всю систему. Она, в частности, не управляет двигателями робота и не может реагировать непосредственно на входную информацию, предъявляемую в виде изображений. Какой частью должна она быть. Сколь сложно организовать ее взаимодействие с остальными программами. [2]
Где же пользователи, заинтересованные в системе доказательства теорем. [3]
В общем случае автоматический решатель задач и система доказательства теорем терпят неудачу при отыскании решения не по причине нехватки времени, а из-за ограниченного объема памяти, которым они могут располагать. Эрнст подчеркивал этот аспект в связи с GPS, а у меня есть подобный же опыт с системой QA3, основанной на логике резолюций. [4]
В предыдущем разделе мы привели целый ряд причин, по которым система доказательства теорем не в состоянии удовлетворительным образом воспроизводить необходимую систему знаний и потому не удовлетворяет требованиям, предъявляемым к системе искусственного интеллекта. Однако подтверждаются ли наши критические замечания на практике. [5]
Итак, в единственном иследовательском центре, обладающем реальным опытом применения системы доказательства теорем для управления робот ом, роль последней становится все менее и менее значительной. [6]
Кажется странным, что столь мощные процедуры выну ждены обращаться к системе доказательства теорем как подпрограмме. Так, например, программа, диагностирующая ошибки системы доказательства теорем, на самом деле будет полностью занята определением возможных путей развития доказательства. [7]
В настоящее время язык, на котором можно выразить эти стратегические сведения в системе доказательства теорем, является исключительно скудным. В лучшем случае он включает эвристические оценочные функции и упорядочения формул ( функции выбора), а они, как мы убедились выше, должны определяться локальными синтаксическими признаками формул. [8]
Совершенно не ясно, могут ли эти программы работать в режиме взаимодействия с системой доказательства теорем. [9]
Некоторые из такого рода описаний действительно можно рационально сформулировать в виде исходных аксиом для системы доказательства теорем. Например, этот план стоит попробовать применить при таких-то обстоятельствах или если вы использовали такой-то факт, то вам, вероятно, потребуется следующее. Этот вид информации присутствует в стратегии, определяющей характер тех процедур логического вывода, которыми следует воспользоваться, - можно было бы сказать если данное символическое выражение решено, примените такую-то вычислительную процедуру и попытайтесь получить решение, используя формулу такого-то типа. Информация такого характера необходима при работе в любой проблемной области. [10]
Большинство языков логического программирования, которые по существу есть ни что иное, как системы доказательства логических теорем, использующие метод резолюций, рассматриваются нами как первые шаги в направлении оптимального логического программирования. [11]
Создается впечатление, что никто еще никогда не пытался получить интересную теорему, выведенную собственно системой доказательства теорем ( хотя была масса разговоров на эту тему), не считая случаев работы с такой системой в режиме взаимодействия. [12]
Можно, конечно, утверждать, что при наличии хороших эвристик логический вывод будет выполняться не системой доказательства теорем, а какой-то другой программой, однако при этом мы сталкиваемся с проблемами организации взаимодействия, которые обсуждаются ниже. Некая программа будет решать, что должно использоваться - эвристическая программа или система доказательства теорем, которые должны находиться во взаимодействии друг с другом. [13]
Не все направления решения задач в области ИИ следовали обрисованному выше пути - Пример несколько иного подхода дают работы по системам доказательства теорем. Здесь идеи, заимствованные из математики и логики, сильно повлияли на направление исследований. Поскольку полнота редко может быть доказана для эвристических методов поиска с выбором первой лучшей вершины или для многих видов селективных генераторов, то ре; зультат этого требования был весьма разочаровывающим. [14]
Их робот управлялся системой доказательства теорем ( типа QA3), и существует фильм, демонстрирующий способность этого робота принять решение об использовании наклонной плоскости для того, чтобы взобраться на ящик. [15]