Алгоритм поиска вывода для натурального классического исчисления высказываний.

Abstract

В статье будет изложен в идейном плане алгоритм поиска вывода для натурального исчисления классической логики высказываний. Своеобразие этого алгоритма, реализованного на языке “Си” для IBM PC, состоит в том, что авторам удалось формализовать эвристики, которые, как нам кажется, применяются в естественном рассуждении. Это позволило найти эффективную процедуру для осуществления субординатных выводов. Система, которая была взята за основу, представляет собой следующее натуральное классическое исчисление высказываний.