Главная страница Случайная страница Разделы сайта АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника |
Исчисление секвенций ИС.
Исчисление высказываний генценовского типа называется исчислением секвенций ИС. Алфавит ИС состоит из символов алфавита ИВ, дополненных символом |-. Допустимые последовательности символов – формулы определяются также как и в ИВ, кроме того, в ИС вводится понятие секвенция. Пусть U1, U2,..., Un, V – формулы ИС. Секвенциями называются конечные последовательности следующих двух видов: 1) U1, U2,..., Un |- V (из истинности U1, U2,..., Un следует истинность V); 2) U1, U2,..., Un |- (система формул U1, U2,..., Un противоречива). Множество аксиом ИС определяется единственной схемой секвенций U |- U. Правила вывода ИС определяются следующими записями, где T, T 1 – конечное множество формул (возможно пустое). 1. (введение Ù). 2. (удаление Ù). 3. (удаление Ù). 4. (введение Ú). 5. (введение Ú). 6. (удаление Ú или правило разбора двух случаев). 7. (введение ®). 8. (удаление ®). 9. (удаление Ø или доказательство от противного). 10. (выведение противоречия). 11. (перестановка посылок). 12. (уточнение или правило лишней посылки). Исчисления ИВ и ИС эквивалентны.
|