Cтраница 3
Рассмотренное нами модальное исчисление высказываний удобно в эвристическом смысле благодаря наличию простого соответствия между ним и одноместным исчислением предикатов первого порядка. Однако, ввиду своей силы, оно является в некотором смысле тривиальной системой. Поэтому интересно было бы рассмотреть более слабые системы, в которых модальность и строгие связки характеризовались бы менее узкими условиями. [31]
Лямбда-исчисление является скорее функциональным, чем исчислением отношений, и в этом состоит различие между ним и исчислением предикатов первого порядка. Так, отец - это функциональное отношение, а брат - более общее отношение, поскольку каждый человек может иметь только одного отца, а братьев может быть несколько. Ниже в этой главе мы более подробно остановимся на связях между языком LISP и лямбда-исчислением. [32]
Известно, что для исчисления предикатов первого порядка не существует общего метода установления общезначимости любых формул, т.е. исчисление предикатов первого порядка является неразрешимым. Однако если некоторая формула исчисления предикатов общезначима, то существует процедура для проверки ее общезначимости, т.е. исчисление предикатов можно назвать полу разрешимым. [33]
В качестве языка представления знаний ( отдельно рассматриваются языки представления эмпирических и теоретических утверждений) используется модификация языка исчисления предикатов первого порядка с обобщенными кванторами. [34]
Понятия абстракции, m - абстракции и ограниченной ш-аб-стракции приводят к широкому спектру новых единообразных полных процедур доказательства для исчисления предикатов первого порядка. Вероятно, такие же стратегии с небольшими изменениями применимы и к логикам более высокого порядка. Эта техника является более общей, чем использование современных единообразных процедур доказательства. Иными словами, каждый вывод контролируется более осмысленным образом структурой задачи в целом, а не локальными свойствами участвующих в выводе дизъюнктов. К тому же при завершении поиска число абстрактных дизъюнктов более ограниченно, чем в середине, поскольку абстракция целевого дизъюнкта должна быть выведена за небольшое число шагов. [35]
Непосредственно из определения позитивно условных термов замечается, что позитивно-условно термальные функции определимы бескванторными позитивными у-функциональными, у-зависимыми формулами исчисления предикатов первого порядка. [36]
Каждому предложению ЕЯ могут быть поставлены в соответствие одна или несколько интерпретаций в формальном языке ( например, в исчислении предикатов первого порядка), для которого определены правила рассуждений. Таким образом, изучение смысла включает: а) перевод предложений ЕЯ в соответствующие формальные структуры; б) рассмотрение логических правил, связываемых с этими структурами. [37]
Учитывая, что невозможно кратко и на поверхностном уровне изложить описание логических моделей представлений знаний, в том числе и исчисления предикатов первого порядка, мы их опускаем. Желающим более детально ознакомиться с вопросами построения логических моделей представления знаний рекомендуем работы [70 - 73], хотя они - не единственные источники информации по этому вопросу. [38]
В статье Some trends in automated reasoning ( Некоторые тенденции в автоматическом поиске вывода) описан алгоритм автоматического доказательства теорем исчисления предикатов первого порядка, предложенный А. Г. Драгалиным и реализованный группой его сотрудников в Дебрецене. Общая схема соответствует методу метапеременных. [39]
Были построены исчисления, в рамках к-рых удалось полностью формализовать св-во универсальной общезначимости формул логики предикатов первого порядка - таковым является исчисление предикатов первого порядка. [40]
Непосредственно из определения условных термов замечается, что условно термальные функции определимы бескванторными у - функциональными, у - зависимыми формулами исчисления предикатов первого порядка. [41]
Однако Ньюэлл, Шоу и Саймон интересовались эвристическими методами, тогда как Ван Хао, а также Гилмор ( программа которого работала с исчислением предикатов первого порядка) ищут алгоритмы, которые давали бы, хотя и в меньшей степени, чем решающая процедура, интересные доказательства за приемлемое время. Как Ван Хао, так и Гилмор пришли к выводу, что для более сложных формальных систем требуются эвристики ( они предпочитают слово стратегии), которые необходимы им для того, чтобы сделать их алгоритмы достаточно селективными для получения интересных доказательств за приемлемое машинное время и при приемлемом объеме памяти. [42]
Очевидно, что любая РСТ-функция ( Э СТ - функция, ЕСТ-функция) определима некоторой бескванторной ( некоторой 3-формулой, некоторой элементарной формулой) исчисления предикатов первого порядка. Представляет интерес описание формул исчисления предикатов, определяющих РСТ ( 3 СТ ЕСТ) - функции, подобное приведенному выше для СТ-функций. [43]
Спецификации выбора числа остаются, конечно, такими же, как и раньше; требованиям различения также можно придать абсолютно точный смысл, поскольку в исчислении предикатов первого порядка у нас имеется естественное понятие различения для дескрипторов: они раз - личны, если ке применимы в точности к одним и тем же вещам. Обобщить требование различения на случай выборов произвольного числа достаточно просто, и мы предоставляем это читателю. [44]
Спецификации выбора числа остаются, конечно, такими же, как и раньше; требованиям различения также можно придать абсолютно точный смысл, поскольку в исчислении предикатов первого порядка у нас имеется естественное понятие различения для дескрипторов: они различны, если не применимы в точности к одним и тем же вещам. Обобщить требование различения на случай выборов произвольного числа достаточно просто, и мы предоставляем это читателю. [45]