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