Специальное исчисление высказываний — различия между версиями
м |
м |
||
Строка 53: | Строка 53: | ||
[[файл:СИВ24.png]] | [[файл:СИВ24.png]] | ||
− | === ''' | + | === '''Пример_з''' === |
[[файл:СЕК30з.JPG]] | [[файл:СЕК30з.JPG]] | ||
− | === ''' | + | === '''Пример_и''' === |
[[файл:СЕК30и.JPG]] | [[файл:СЕК30и.JPG]] | ||
− | === ''' | + | === '''Пример_к''' === |
[[файл:СЕК30к.JPG]] | [[файл:СЕК30к.JPG]] | ||
− | === ''' | + | === '''Пример_л''' === |
[[файл:СЕК30л.JPG]] | [[файл:СЕК30л.JPG]] | ||
− | === ''' | + | === '''Пример_м''' === |
[[файл:СЕК30м.JPG]] | [[файл:СЕК30м.JPG]] | ||
− | === ''' | + | === '''Пример_н''' === |
[[файл:СЕК30н.JPG]] | [[файл:СЕК30н.JPG]] | ||
− | === ''' | + | |
+ | === '''Пример_о''' === | ||
[[файл:СЕК30о.JPG]] | [[файл:СЕК30о.JPG]] | ||
+ | [[файл:СИВ31.png]] | ||
=== '''Правило_п''' === | === '''Правило_п''' === | ||
[[файл:СЕК30п.JPG]] | [[файл:СЕК30п.JPG]] | ||
+ | [[файл:СИВ32.png]] | ||
== [[Логические понятия|Другие понятия:]] == | == [[Логические понятия|Другие понятия:]] == | ||
{{Список ЛП}} | {{Список ЛП}} |
Версия 11:54, 4 апреля 2025
Специальное исчисление высказываний (секвенций) — построение логической последовательности условных суждений (секвенций) по определённым правилам. В секвенциальном подходе используется аксиома и правила вывода, а доказательство ведётся в форме дерева вывода. Исчисления секвенций относятся к генценовскому типу.
Содержание
Обозначения
A, B, C — одиночные формулы;
Γ, Г1, Г2 — списки формул антецедента, возможно пустые;
A1, A2, …, An — формулы списка антецедента;
B1, B2, …, Bm — формулы списка антецедента;
Ø — пустое множество формул;
├ — знак вывода;
W –– ослабление;
P –– перестановка;
˄ –– конъюнкция;
˅ –– дизъюнкция;
¬ –– отрицание;
→ –– импликация.
Определения
Секвенции (латинское sequentia — последовательность, следствие) — это выражения вида A1, A2,..., Am |- B1, B2,..., Bn, где |- — знак выводимости, A1, A2,..., Am и B2,..., Bn — произвольные формулы; первые — образующие антецедент секвенции, вторые — её сукцедент. Такого рода выражения изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать).
Аксиома
Основные правила
Дополнительные правила
Примеры
Доказательства секвенций
Пример_в
Пример_д
Пример_е
Пример_ж
Пример_з
Пример_и
Пример_к
Пример_л
Пример_м
Пример_н
Пример_о
Правило_п
Другие понятия:
Ссылки
- Генцен Г. Исследования логических выводов. В кн. Математическая теория логического вывода, М, 1967, с. 9—74.
- Участник:Logic-samara