Другое: Натуральный вывод
Описание
Характеристики учебной работы
Список файлов
- Натуральный вывод.TXT 2,92 Kb
- Прочти меня!!!.txt 136 b
НАТУРАЛЬНЫЙ ВЫВОД
---------------------------------------- ------------------------------------
Правила НАТУРАЛЬНОГО ВЫВОДА.
Конъюнкция:
F1 F2 F1 & F2 F1 & F2
&i ------- &e1 ------- &e2 -------
F1 & F2 F1 F2
Дизъюнкция:
[F1] [F2] [F1] [F2]
F1 F2 F1VF2 F3 F3
Vi1 ------- Vi2 ------- Vi3 ------- Ve ----------------
F1 V F2 F1 V F2 F1 V F2 F3
Импликация:
[F1] [F3] [F2]
F2 F1>F2 F1 F1>F2 F1 F3
>i ------- >e1 --------- >e2 ----------------
F1 > F2 F2 F3
Отрицание и ложь:
[F] [F]
F F
i ------ i --- e ---
F F
Кванторы: [(Svw)F]
(Svw)F A.v F (Svt)F E.v F F1
Ai+ ------ Ae- ------ Ei- ------ Ee+ -----------
A.v F (Svt)F E.v F F1
Обозначения: w - константа, не встречающаяся в заключениях Ee+ и Ai+ и
гипотезах, от которых эти заключения зависят; t - терм, свободный для v в F;
(Sxy)F - подстановка: в F заменить x на y.
---------------------------------------- ------------------------------------
Правила ПОИСКА НАТУРАЛЬНОГО ВЫВОДА.
Конъюнкция: Дизъюнкция:
&ai |- F1&F2 => |-F1 / |-F2 Vai |- F1VF2 => F1;F2 |-
&si F1; F2 => F1&F2 Vae F1VF2 |- F3 => F1|-F3 / F2|-F3
&se1 F1&F2 => F1 Vsi1 F1 => F1VF2
&se2 F1&F2 => F2 Vsi2 F2 => F1VF2
Импликация: Отрицание и ложь:
>ai |- F1>F2 => F1|-F2 si F; F =>
>ae2 F1>F2|-F3 => F3|-F1 / F2|-F3 del |- F =>
>ae F1>F2 |-F2 => |-F1 ai |- F => F |-
>si F2 => F1>F2 ae1 |- F => F |-
>se F1>F2; F1 => F2 ae2 F|- => |-F
Кванторы:
Aai+ |- A.vF => |- (Svw)F w - новая константа
Ase A.vF => (Svt)F t - терм, свободный
Eai |- E.vF => E.vF |- (Svt)F для v в формуле F
Esi F => E.v (Stv)F
Ese+ E.vF => (Svw)F
---------------------------------------- ------------------------------------
Файл скачан с сайта StudIzba.com
При копировании или цитировании материалов на других сайтах обязательно используйте ссылку на источник
Начать зарабатывать