Другое: Секвенциальное исчисление
Описание
Характеристики учебной работы
Список файлов
- Прочти меня!!!.txt 136 b
- Секвенциальное исчисление.txt 1,61 Kb
Файл скачан с сайта StudIzba.com
При копировании или цитировании материалов на других сайтах обязательно используйте ссылку на источник
СЕКВЕНЦИАЛЬНОЕ ИСЧИСЛЕНИЕ
---------------------------------------- ------------------------------------
Аксиома СЕКВЕНЦИАЛЬНОГО ВЫВОДА.
F1, L -> R, F1
---------------------------------------- ------------------------------------
Правила СЕКВЕНЦИАЛЬНОГО ВЫВОДА.
Конъюнкция:
F1,F2,L->R L->R,F1 L->R,F2
(&<-) ---------- (->&) -----------------
F1&F2,L->R L->R,F1&F2
Дизъюнкция:
F1,L->R F2,L->R L->R,F1,F2
(V<-) ----------------- (->V) ----------
F1VF2,L->R L->R,F1VF2
Импликация:
L->R,F1 F2,L->R F1,L->R,F2
(><-) ----------------- (->>) ----------
F1>F2,L->R L->R,F1>F2
Отрицание:
L->R,F1 F1,L->R
(¬<-) -------- (->¬) --------
¬F1,L->R L->R,¬F1
Кванторы:
A.vF1,(Svt)F1,L->R L->R,(Svw)F1
(A<-) ------------------ (->A) ------------
A.vF1,L->R L->R,A.vF1
(Svw)F1,L->R L->R,(Svt)F1,E.vF1
(E<-) ------------ (->E) ------------------
E.vF1,L->R L->R,E.vF1
Обозначения:
F1 и F2 - формулы, L и R - списки формул;
w - константа, не встречающаяся в заключениях правил ->A и E<-;
t - терм, свободный для v в F1;
(Sxy)F1 - подстановка: в F1 заменить x на y.
---------------------------------------- ------------------------------------
Начать зарабатывать