Специальное исчисление высказываний — различия между версиями
м |
м |
||
Строка 67: | Строка 67: | ||
=== '''Пример_о''' === | === '''Пример_о''' === | ||
− | [[файл:СЕК30о.JPG]] | + | <!--[[файл:СЕК30о.JPG]]--> |
[[файл:СИВ31.png]] | [[файл:СИВ31.png]] | ||
=== '''Пример_п''' === | === '''Пример_п''' === | ||
− | [[файл:СЕК30п.JPG]] | + | <!--[[файл:СЕК30п.JPG]]--> |
[[файл:СИВ32.png]] | [[файл:СИВ32.png]] | ||
== [[Логические понятия|Другие понятия:]] == | == [[Логические понятия|Другие понятия:]] == |
Версия 12:11, 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