ЕСТЕСТВЕННЫЙ ЛОГИЧЕСКИЙ ВЫВОД

ЕСТЕСТВЕННЫЙ ЛОГИЧЕСКИЙ ВЫВОД — формальный вывод, по возможности приближенный к содержательному рассуждению, привычному для математика и логика. Критерии естественности и качества вывода не уточняются полностью, но обычно имеются в виду выводы, осуществляемые по общеупотребительным правилам логических переходов, компактные (в частности, не содержащие излишних применений правил вывода), «склеенные» (повторяющиеся участки выводов должны устраняться, напр., при помощи вычленения вспомогательных лемм) и др.

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

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

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

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

С. Ю. Маслов.

Источники:

1. Математическая энциклопедия: Гл. ред. И. М. Виноградов, т. 2 Д - Коо.-М.: «Советская Энциклопедия», 1979.-1104 стб., ил.