Суппес–леммоновская нотация
-
Основы естественного вывода
- Естественный вывод — это метод доказательства теорем, основанный на правилах и предположениях.
- Правила естественного вывода включают аксиомы, правила вывода и правила введения и исключения.
- Правила вывода включают modus ponens, modus tollens, правило двойного отрицания и другие.
-
Примеры и правила
- Примеры включают доказательство принципа взрыва и использование монотонности следования.
- Правила включают допущения, условное доказательство, двойное отрицание и другие.
- Правила позволяют выводить новые правила из существующих.
-
Историческое развитие
- Куайн использовал номера строк для обозначения зависимостей в 1940 году.
- Суппес ввел звездочки для обозначения зависимостей в 1957 году.
- Столл использовал наборы номеров строк для обозначения зависимостей в 1963 году.
- Леммон представил метод Суппеса в учебнике 1965 года.
- Клини кратко описал два вида практических логических доказательств в 1967 году.
-
Рекомендации и внешние ссылки
- Статья содержит перевод «Исследования логической дедукции» Сабо.
- Ссылки на учебники по истории естественной дедукции и элементарной логике.