Одним из аргументов в пользу эффективности такого перехода к новому метаязыку может служить следующий факт из истории математики, когда за счет перехода к «языку метапеременных) Х и У» удалось найти общий метод решения квадратных уравнений. Обобщая этот подход можно сформулировать следующее методологическое правило, активным приверженцем и пропагандистом которого был крупный российский философ и логик В.А. Смирнов: переформулировка задачи на новом языке (метаязыке) позволяет существенно упростить процедуру ее решения, а часто просто превращает сложную задачу в тривиально решаемую. Достаточно нагляден в этом отношении и следующий пример, приводимый в [8]. Пусть нам дано аксиоматическое исчисление:

аксиома 1: A=A A [B], B = С

аксиома 2: (A=B)=(B= А) правило вывода: ------------------- ,

аксиома 3: (A=(B=C) = ((A = B)= С) А [С]

в котором необходимо построить вывод формулы W: (P= Q) = ((Q = R) = (R = P))

Вывод формулы W в данном исчислении занимает около двух страниц. Однако Р. Вейхрауху удалось значительно упростить данную задачу, предложив следующее правило (метаправило) для исчислений подобного типа: Каждое высказывание W, построенное только из пропозициональных переменных с помощью связки эквивалентности "=" таким образом, что любая пропозициональная переменная p входит в W четное число раз (выделено мной — К.С.), является теоремой [9].

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

В рамках реализации этой идеи было сделано следующее:

· переход к логическим исчислениям, использующим тернарные логические связки. В рамках проекта этот подход реализован построением исчисления поиска на базе тернарной связки «условной дизъюнкции» [10]. Отметим, что идея использования этой связки при построении логических исчислений восходит к А. Черчу [11], а впервые была реализована в работе российского логика Е. Сидоренко [12]);

· переход к логическим исчислениям с «временными» переменными (мета-переменными). В рамках проекта этот подход реализован в работе [13]. Отметим, что в данном случае сформулированное выше методологическое правило конкретизируется так: введение новых объектов (путем использования «временных» метапеременных), которые замещают фиксированные значения переменных «нижнего» уровня (авторство этой идеи принадлежит С. Кангеру [4], Д. Правицу и Н. Шанину [5, стр.100]);

Во-вторых, при построении «логико — эвристических» исчислений целесообразно превратить их в формульно-ориентированные метаисчисления, т.е. использовать идею «глобальной обработки информации», предложенную в рамках ленинградской школы математической логики (пионерские реализации этой идеи представлены в работах [14, 15]). Суть этого подхода заключается в том, чтобы при построении вывода формулы использовать дополнительную информацию о структуре формулы (структурной информации) удается поиск вывода организовать более эффективно. Для этого создаваемые метаисчисления должны не только «наследовать» свойства исходных исчислений, но и учитывать особенности выводимых формул, т.е. быть формульно-ориентированными. В этом смысле исчисления поиска вывода можно трактовать как метаисчисления Иb,f, построенного по исходному исчислению b и формуле f. Выводимость в построенном метаисчислении особого объекта Џ эквивалентна выводимости f в исходном исчислении b. К этому классу исчислений можно отнести исчисления обратного метода [16], исчисления метода резолюций [17] и расщеплений [18], а также построенные С. Катречко исчисления чисел с индексами [19, 20, 21]. В рамках реализации этой идеи было сделано следующее:

· построение машинной реализации исчислений чисел с индексами для пропозициональной логики (см. распечатку текста программы, написанной на языке СИ++ в приложении 1), в рамках которой предложен оригинальный алгоритм преобразования формул в д. н. ф. [22, 23];

· в общих чертах сформулированы принципы написания программы автоматического доказательства теорем на базе предложенного исчисления чисел с индексами для исчисления предикатов [20, 23, 24];

· сформулирована оригинальная идея о возможности повышения эффективности исчислений поиска за счет перехода к новой структуре представления формул и выводов. Первоначально эта идея была высказана [25], как идея возможности структурной специализации выводов в секвенциальных системах и системах натурального вывода. Чуть позже она была использована при построении исчислений с «условной дизъюнкцией». В рамках данного проекта она получила дальнейшее развитие при формулировании оригинального алгоритма перевода формулы в дизъюнктивной нормальной форме в качестве использования более компактного представления д.