Akademik

-формальный вывод, по возмвжности приближенный к содержательному рассуждению, привычному для математика и логика. Критерии естественности и качества вывода не уточняются полностью, но обычно имеются в виду выводы, осуществляемые по общеупотребительным правилам логических переходов, компактные (в частности, не содержащие излишних применений правил вывода), "склеенные" (повторяющиеся участки выводов должны устраняться, напр., при помощи вычленения вспомогательных лемм) и др.

Первоначально формализации логических и математич. теорий не преследовали целей естественности (см. Логические исчисления);решающее продвижение в этом направлении составило исчисление натуральных выводов (см. Генцена формальная система), имитирующее форму обычных математич. умозаключений и позволяющее вводить и использовать допущения привычным образом. Довольно естественно выглядят и приемы обращения с допущениями в секвенциальных исчислениях, к-рые обладают дополнительным преимуществом - подформульности свойством и поэтому лежат в основе дальнейших продвижений в проблеме построения Е. л. в.

Для автоматизации поиска Е. л. в. были предложены [2] вспомогательные секвенциальные исчисления, обладающие свойством подформульности, но запрещающие переход допущений в сукцедент (см. Секвенция). По выводу в таком исчислении легче строить Е. л. в. На этой основе была разработана методика поиска Е. л. в., включающая учет "родственностей" (т. е. равных подформул в составе испытуемых формул) для сокращения выводов и их "склеивания", "прополку" излишних формул и применений правил, возможность варьирования тактик установления выводимости и др. В рамках логических средств классического высказываний исчисления эта методика была доведена до машинного алгорифма (программа находила Е. л. в. данного утверждения из данного списка гипотез и записывала этот вывод в виде логико-математич. текста на русском языке). К проблеме поиска Е. л. в. примыкают задачи корректирования гипотез и усиления теорем (речь идет о методах, позволяющих вводить в заданную формулу небольшие исправления так, чтобы она стала теоремой или превратилась в более сильную теорему, и об исследовании критериев качества таких исправлений).

Разработки в области Е. л. в. в основном посвящены классич. логикам, но возникшие методы носят более общий характер.

Лит.:[I] Математическая теория логического вывода, сб. переводов, М., 1967; [2] Шанин Н. А. и др., Алгорифм машинного поиска естественного логического вывода в исчислении высказываний," М.- Л., 1965; [3] Рrawitz D., Natural deduction, Stockh., 1965.

С. Ю. Мослов.