Cтраница 4
Он использует точные рассуждения, и это неудивительно. Кроме всего прочего, Пролог основан на традициях логического программирования и автоматического доказательства теорем. В такой среде знание определенных фактов абсолютно, а из них уже выводятся другие абсолютные факты. Если вы желаете использовать вероятностное оценивание, то необходимо встроить соответствующие средства. [46]
В этой заключительной главе рассмотрим некоторые открытые вопросы, относящиеся к автоматическому доказательству теорем. [47]
Общая идея, состоящая в рассмотрении логических предложений как операторов в программах, а управляемого вывода - как исполнения программ, была исследована Хайсом ( 1973), Сандвеллом ( 1973) и другими. Это было существенное продвижение вперед, необходимое для адаптации понятий из области автоматического доказательства теорем к методам вычислений, уже понятным программистам. [48]
Генцен, ни разу не был упомянут) Этот недостаток отчасти восполняется примечаниями редактора и Дополнением А, содержащим, в частности, эскиз идейного развития области, включая объяснение сути генценовских методов. Дополнение А ( и отчасти В) содержит также информацию о другом методе автоматического доказательства теорем, появившемся одновременно с методом резолюций. [49]
Хотя в каждом из наших примеров применялась одна и та же программа AURA [19] ( разработанная совместно Аргон-нской национальной лабораторией и Университетом Северного Иллинойса), многочисленные исследования показывают, что такого же рода результаты могли бы быть получены с помощью других программ для доказательства теорем. Помня об этом, мы можем с уверенностью заявить, что в области автоматического доказательства теорем достигнута важная цель - программы, доказывающие теоремы, могут с успехом применяться в различных областях. [50]
Природа этого скептицизма заставила нас поставить в этой работе и другую цель: преодолеть, хотя бы частично, сопротивление, возникающее на пути такого рода автоматизации. Мы обсудим два основных заблуждения, на которых основана неверная оценка полезности и потенциальных возможностей автоматического доказательства теорем. Опровергнув эти заблуждения, мы устраним существенное препятствие к тому, чтобы программа автоматического доказательства теорем играла свою истинную роль - роль коллеги и помощника. [51]
Но данное множество является подмножеством общего множества дизъюнктов, в которое входит около 200 дизъюнктов. Таким образом, нахождение именно этого невыполнимого подмножества и его последовательное опровержение является сложной задачей для процедуры автоматического доказательства теорем. [52]
Система должна обладать необходимыми средствами для выявления и устранения таких противоречий. В системах, построенных на основе применения логистического подхода, вопрос о наличии противоречий разрешается при помощи алгоритмов автоматического доказательства теорем. [53]