Логика предикатов
Категория реферата: Рефераты по философии
Теги реферата: bestreferat ru, роботы реферат
Добавил(а) на сайт: Пондяков.
Предыдущая страница реферата | 1 2 3 4 5 6 7 8 9 10 | Следующая страница реферата
2. Если A есть аксиома, то A есть вывод из пустой последовательности посылок, A есть его последняя формула и входит в вывод.
3. Если a есть вывод из последовательности посылок G и A посылка, то
есть вывод из последовательности посылок GA, A есть его последняя формула и формула B входит в вывод, если B входит в a или графически равно формуле A.
4. Если a есть вывод из последовательности посылок G, формула C непосредственно выводима из формул, входящих в a ( или является аксиомой), то
есть вывод из последовательности посылок G, C его последняя формула и B входит в вывод, если оно входит в a или графически равно C. На применение правила введения квантора общности накладываем ограничение: если a есть вывод из последовательности посылок G, формула A(w) входит в вывод a, но в формулы из G не входит собственная переменная w, то
a
"xFw/x A(w)
есть вывод из последовательности посылок G.
5. Если a есть вывод из последовательности посылок G и b есть вывод из посылок D,A и все формулы из D входят в a, B есть последняя формула, то
есть вывод из посылок G и AÉB есть его последняя формула.
6. Если a есть вывод из посылок G, b есть вывод из посылок D1,A и g есть вывод из посылок D2,B,формулы D1 и D2 входят в a, формула C есть последняя формула b и g, то
есть вывод из посылок G и C есть его последняя формула.
7. Если a есть вывод из последовательности посылок G,A и ^ есть его последняя формула, то
есть вывод из посылок G и ØA есть его последняя формула.
Чтобы определение вывода NeC было полным необходимо сформулировать прямые правила вывода. Прежде всего есть правило тождественного перехода: из A выводима A, обозначим его буквой I. Остальные правила вывода подразделяются на правила введения и удаления логических констант. В приводимой ниже таблице правил вывода мы для полноты записываем и непрямые правила (хотя они сформулированы в определении вывода).
Кроме основных будем использовать в качестве официальных также два производных правила Éе1 и Éi2:
и
Теперь перейдем к процедуре писка вывода. Поиск начинается с формулировки задачи: из посылок A1,...,An требуется вывести формулу В. Мы исходим из допущения, что ни посылки, ни заключение не содержат e-символов и предиката существования. Не нарушая общности можно также допустить, что они не содержат свободных переменных. Задача поиска вывода записывается в виде
Это, естественно, не вывод. Построение ( поиск ) вывода совершается с помощью двух типов шагов: синтетических и аналитических. Синтетический шаг состоит в применении некоторого прямого правила вывода. Аналитический шаг сводит задачу к подзадачам.
Рекомендуем скачать другие рефераты по теме: сочинение изложение, курсовые работы бесплатно.
Предыдущая страница реферата | 1 2 3 4 5 6 7 8 9 10 | Следующая страница реферата