ВУЗ:
Составители:
Рубрика:
7
некоторого словаря, или деталей из некоторого набора. Для множества T
существует некоторый способ определения принадлежности или
непринадлежности произвольного элемента к данному множеству.
Процедура такой проверки может быть любой, но она должна давать ответ на
вопрос, является ли x элементом множества T за конечное число шагов.
Обозначим эту процедуру P(T).
Множество
S есть множество синтаксических правил. С их помощью
из элементов T образуют синтаксически правильные совокупности.
Например, из слов словаря строятся синтаксически правильные фразы, а из
деталей собираются конструкции. Существует некоторая процедура P(S), с
помощью которой за конечное число шагов можно получить ответ на вопрос,
является ли совокупность X синтаксически правильной.
Во множестве синтаксически правильных
совокупностей выделяется
некоторое подмножество A. Элементы A называются аксиомами. Как и для
других составляющих формальной системы, должна существовать процедура
P(A), с помощью которой для любой синтаксически правильной
совокупности можно получить ответ на вопрос о принадлежности ее к
множеству A.
Множество B есть множество правил вывода. Применяя их к
элементам A, можно получать новые синтаксически правильные
совокупности,
к которым снова можно применять правила из B. Так
формируется множество выводимых в данной формальной системе
совокупностей. Если имеется процедура P(B), с помощью которой можно
определить для любой синтаксически правильной совокупности, является ли
она выводимой, то соответствующая формальная система называется
разрешимой. Это показывает, что именно правила вывода являются наиболее
сложной составляющей формальной системы
.
Исчисление высказываний является разрешимой формальной
системой, а исчисление предикатов первого порядка – неразрешимой
формальной системой.
С накоплением опыта построения формальных теорий и попытками
аксиоматизации арифметики, предпринятыми Дж. Пеано, возникла теория
доказательств. Теория доказательств – это раздел современной
математической логики и предшественница логического программирования.
1.2 Автоматизация доказательства в логике предикатов.
1.2.1 История вопроса
Поиск
общей разрешающей процедуры для проверки общезначимости
формул был начат Лейбницем в XVII веке. Затем исследования
продолжились в XX веке, а в 1936 году Черч и Тьюринг независимо друг от
друга доказали, что не существует никакой общей разрешающей процедуры,
никакого алгоритма, проверяющего общезначимость формул в логике
предикатов первого порядка.
Страницы
- « первая
- ‹ предыдущая
- …
- 5
- 6
- 7
- 8
- 9
- …
- следующая ›
- последняя »
