Математическое введение в декларативное программирование. Зюзысов В.М. - 20 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

Составители: 

Рубрика: 

• Формальная теория T называется полной (относительно данной интерпретации), если
каждому истинному высказыванию об объектах M соответствует теорема теории T .
• Если для предметной области M существует формальная полная непротиворечивая
теория T, то M называется аксиоматизируемой (или формализуемой).
• Система аксиом (или аксиоматизация) формально непротиворечивой теории T называ-
ется независимой, если никакая из аксиом не выводима из остальных по правилам
вывода теории T.
Одним из первых вопросов, которые возникают при задании формальной теории,
является вопрос о том, возможно ли, рассматривая какую-нибудь формулу формальной
теории, определить, является ли она доказуемой или нет. Другими словами, речь идет о
том, чтобы определить, является ли данная формула теоремой или не-теоремой и как это
доказать.
• Формальная теория T называется разрешимой, если существует алгоритм, который
для любой формулы теории определяет, является ли это формула теоремой теории.
• Формальная теория T называется полуразрешимой, если существует алгоритм, кото-
рый для любой формулы P теории выдает ответ «да», если P является теоремой теории
и выдает «нет» или, может быть, не выдает никакого ответа, если P не является теоре-
мой (то есть алгоритм применим не ко всем формулам).
2.5 Примеры формальных теорий
Приведем несколько примеров формальных теорий из книги Хофштадтера [9].
Формальная система MIU
Алфавит: M, I, U.
Формулы = {M, I, U}*.
Аксиома: MI.
Правила вывода:
1). xI → xIU (продукция);
2). Mx → Mxx (продукция);
3). III → U (правило переписывания);
4). UU → ∅ (правило переписывания, ∅ обозначает пустую последовательность).
Продукция – правило, применяемое к формулам, рассматриваемым как единое целое. •
• Правило переписывания – правило, которое может применяться к любой подформуле
формулы.
Приведем типичный вывод в этой теории:
MI Аксиома
MII Правило 2
MIIII Правило 2
MUI Правило 3
MUIU Правило 1
MUIUUIU Правило 2
MUIIU Правило 4
Любые утверждения о свойствах этой теории являются метатеоремами. Предлагается чи-
тателю задача: «Найдите вывод MU или докажите, что он невозможен».
Формальная система PR
Алфавит: {P, R, –}
Выражения – элементы {P, R, –}*.
20

Страницы