Естественный Логический Вывод

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

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

В рамках логических средств классического высказываний исчисления эта методика была доведена до машинного алгорифма (программа находила Е. Л. В. Данного утверждения из данного списка гипотез и записывала этот вывод в виде логико-математич. Текста на русском языке). К проблеме поиска Е. Л. В. Примыкают задачи корректирования гипотез и усиления теорем (речь идет о методах, позволяющих вводить в заданную формулу небольшие исправления так, чтобы она стала теоремой или превратилась в более сильную теорему, и об исследовании критериев качества таких исправлений). Разработки в области Е. Л. В. В основном посвящены классич. Логикам, но возникшие методы носят более общий характер. Лит.:[I] Математическая теория логического вывода, сб.

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