Математическая энциклопедия - естественный логический вывод
Связанные словари
Естественный логический вывод
-формальный вывод, по возмвжности приближенный к содержательному рассуждению, привычному для математика и логика. Критерии естественности и качества вывода не уточняются полностью, но обычно имеются в виду выводы, осуществляемые по общеупотребительным правилам логических переходов, компактные (в частности, не содержащие излишних применений правил вывода), "склеенные" (повторяющиеся участки выводов должны устраняться, напр., при помощи вычленения вспомогательных лемм) и др.
Первоначально формализации логических и математич. теорий не преследовали целей естественности (см. Логические исчисления);решающее продвижение в этом направлении составило исчисление натуральных выводов (см. Генцена формальная система), имитирующее форму обычных математич. умозаключений и позволяющее вводить и использовать допущения привычным образом. Довольно естественно выглядят и приемы обращения с допущениями в секвенциальных исчислениях, к-рые обладают дополнительным преимуществом подформульности свойством и поэтому лежат в основе дальнейших продвижений в проблеме построения Е. л. в.
Для автоматизации поиска Е. л. в. были предложены [2] вспомогательные секвенциальные исчисления, обладающие свойством подформульности, но запрещающие переход допущений в сукцедент (см. Секвенция). По выводу в таком исчислении легче строить Е. л. в. На этой основе была разработана методика поиска Е. л. в., включающая учет "родственностей" (т. е. равных подформул в составе испытуемых формул) для сокращения выводов и их "склеивания", "прополку" излишних формул и применений правил, возможность варьирования тактик установления выводимости и др. В рамках логических средств классического высказываний исчисления эта методика была доведена до машинного алгорифма (программа находила Е. л. в. данного утверждения из данного списка гипотез и записывала этот вывод в виде логико-математич. текста на русском языке). К проблеме поиска Е. л. в. примыкают задачи корректирования гипотез и усиления теорем (речь идет о методах, позволяющих вводить в заданную формулу небольшие исправления так, чтобы она стала теоремой или превратилась в более сильную теорему, и об исследовании критериев качества таких исправлений).
Разработки в области Е. л. в. в основном посвящены классич. логикам, но возникшие методы носят более общий характер.
Лит.:[I] Математическая теория логического вывода, сб. переводов, М., 1967; [2] Шанин Н. А. и др., Алгорифм машинного поиска естественного логического вывода в исчислении высказываний," М.Л., 1965; [3] Рrawitz D., Natural deduction, Stockh., 1965.
С. Ю. Мослов.
Математическая энциклопедия. — М.: Советская энциклопедия
И. М. Виноградов
1977—1985
Вопрос-ответ:
Похожие слова
Самые популярные термины
1 | 549 | |
2 | 476 | |
3 | 471 | |
4 | 465 | |
5 | 448 | |
6 | 432 | |
7 | 430 | |
8 | 426 | |
9 | 417 | |
10 | 417 | |
11 | 415 | |
12 | 406 | |
13 | 398 | |
14 | 372 | |
15 | 368 | |
16 | 364 | |
17 | 358 | |
18 | 357 | |
19 | 357 | |
20 | 355 |