Предыдущая страница реферата | 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 | Следующая страница реферата