Теорема корректности для алгоритма поиска вывода в классической логике высказываний. В. Шангин

Logical Studies No.4 (2000)
В. Шангин
Теорема корректности для алгоритма поиска вывода в классической логике высказываний
В данной работе изложено доказательство теоремы корректности для алгоритма поиска вывода в классической логике высказываний, предложенного А.Е.Болотовым, В.А.Бочаровым на основе системы натурального вывода в формулировке В.А.Бочарова и В.И.Маркина. А.Е.Горчаковым разработана компьютерная программа PROVER. Теорема корректности подразумевает, что всякий раз, когда требуется обосновать произвольную выводимость цели из посылок, данный алгоритм или обоснует данную выводимость, построив натуральный вывод, либо опровергнет данную выводимость, построив контрпример. Обратим внимание на следующие особенности доказательства: (1) контрпример конструктивно извлекается из натурального вывода как множество неисключенных литералов; (2) вводится понятие "П-дерева", которое близко идее Н.Н. Непейводы о неполных структурах вывода и их использовании.

по-русски