Обратный метод установления выводимости для логических исчислений

В первой главе описывается некоторая схема действий, направленных на установление выводимости (а затем и на получение вывода) секвенции в том или ином секвенциальном исчислении, обладающем “свойством подформульности”. Схема эта возникает как результат выявления основных черт предложенного автором (ДАН СССР, т. 159, № 6; т. 172, № 1) обратного метода установления выводимости (метод этот предназначен для построения машинных алгорифмов поиска логического вывода). Помимо общей схемы обратного метода, описываются некоторые ее конкретизации для классического исчисления предикатов. Вторая глава содержит применение обратного метода к теории разрешимых фрагментов чистого исчисления предикатов. Приводятся новые обобщающие результаты, этой теории. Библ. 27 назв.