С.), является теоремой [2].

Данное правило позволяет "свести" доказательство некоторой формулы W к простому подсчету "четности" разных переменных, что значительно сокращает "вывод" данной формулы W. Это стало возможным за счет использования при построении вывода новой абстракции — понятия "четное число", которое в языке логики высказываний невыразимо.

С этой точки зрения, представляет интерес подход к построению алгоритмов нахождения общезначимости для пропозициональной логики, предложенный С.Ю.Масловым, который получил название обратный метод [3]. Фактически, исчисления обратного метода представляют из себя метаисчисления, в котором удается выразить информацию о «зацепленности» переменных формулы. Использование этой дополнительной информации позволяет надеяться на построение более эффективных алгоритмов поиска вывода, теоретическая проработка которых велась под руководством Владимира Александровича Смирнова (некоторые из возможных алгоритмов поиска вывода представлены в [4]).

Литература:

1. Маслов С.Ю. Теория поиска вывода и вопросы психологии творчества //Вопросы семиотики, 1979, Вып. 13, С. 17-46

2. Weyhrauch R.W. Prolegomena to a theory of mechanized formal reasoning //Artificial Intelligence, 1980, Vol. 13. P. 133 - 170

3. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР, 1968, Т. 98. С. 26 - 87

4. Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова //Логические методы в компьютерных науках, М., ИФРАН, 1992. С. 125 - 141
С.Л. Катречко

ОТ ЛОГИКИ К ТЕОРИИ ПОИСКА ВЫВОДА

Теория поиска вывода (ТПВ)  молодая область логики, которая, в отличие от логики, акцентирует свое внимание не на вопросе о логической корректности выводов, а на вопросе о способах построения выводов («как строить (искать) вывод?») [1].

Специфику и основные идеи ТПВ покажем на примере построения вывода формулы [р Й р] исчислении P1. [P1 задается тремя аксиомами p Й [q Й p]; [s Й [p Й q]] Й [[s Й p] Й [s Й q]]; p Й f Й f Й p и двумя правилами вывода: - модус поненс и - подстановка; ВЫВОД определяется как последовательность формул, каждая из которых является либо некоторой аксиомой, либо получена из предшествующих формул вывода по одному из правил вывода, последняя формула которой является искомой формулой]. В [2, стр.75] приведена следующая последовательность из 9 формул, являющаяся выводом формулы [р Й р] (приведем вывод с анализом):

ВЫВОД АНАЛИЗ ВЫВОДА

1. [s Й [p Й q]] Й [[s Й p] Й [s Й q]]

2. [s Й [r Й q]] Й [[s Й r] Й [s Й q]] 1, подстановка p/r

3. [s Й [r Й p]] Й [[s Й r] Й [s Й p]] 2, подстановка q/p

4. [p Й [r Й p]] Й [[p Й r] Й [p Й p]] 3, подстановка s/p

5. [p Й [q Й p]] Й [[p Й q] Й [p Й p]] 4, подстановка r/q

6. p Й [q Й p]

7. [p Й q] Й [p Й p] 5, 6

8. p Й [q Й p] Й [p Й p] 7, подстановка q/qЙp

9. p Й p 8, 6

Давайте зададимся вопросом: «Почему на 1 (2, 3... 8) шагах были выбраны те или иные аксиомы, правила вывода и сделаны в случае выбора правила подстановки?», т.е. нас в данном случае интересует не вопрос о корректности построенного вывода, а вопрос об осмыслении процесса построения вывода. Прикладное значение этой постановки вопроса заключается в том, чтобы научить студента или ЭВМ строить подобные выводы.

Основная идея ТПВ - переход к метаисчислениям, в рамках которого появляется возможность учитывать «структурную» информацию логической формулы. Эта идея может быть реализована двумя способами:

· введением собственно допустимых, т.е. не производных, правил вывода, существенно сокращающих длину вывода;

· использованием метода временных переменных (метапеременных), которые вводятся для фиксирования (полной или неполной на данном этапе построения вывода) информации о возможной структуре выводимой формулы, а в последующем, при получении дополнительной необходимой информации, заменяются на переменные (формулы) исходного исчисления.

Остановимся более подробно на втором способе (заметим, что в [2] Черчем реализован первый путь перехода к метаисчислению путем доказательства метатеоремы дедукции, которая выступает как собственно допустимое правило вывода, позволяя вводить (а впоследствии, исключать) допущения). Для этого введем временные метапеременные, которыми при анализе структуры формулы будем заменять отдельные ее переменные (подформулы) так, что каждая эквивалентная переменная (подформула) будет заменяться на одну и ту же временную метапеременную.