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

Начиная с середины ХХ века, в связи с бурным развитием вычислительной техники, наряду с тремя вышеперечисленными критериями логических исчислений необходимо ввести еще один параметр оценки вычислительных систем — критерий эффективности. В отличие от критерия разрешимости, который устанавливает принципиальную (теоретическую) разрешимость логических исчислений, данный критерий является критерием практической эффективности вычислительной системы и призван оценить эффективность (быстроту) вычислительного алгоритма. Тем самым, суть новой проблемы, связанной с развитием вычислительных систем, можно сформулировать в виде задачи перехода от «медленных» процедур полного перебора, имеющих экспоненциальную сложность, к более «быстрым» (эффективным) алгоритмам, идеалом которых являются полиноминальные вычислительные алгоритмы. При этом заметим, что, во-первых, критерий практической эффективности системы в общем случае вступает в конфликт с «полнотой» поисковой процедуры, т.е. с заведомым нахождением всех возможных решений, поскольку эффективность поисковой процедуры предполагает отказ от процедур полного перебора. В этом смысле такие процедуры являются «неполными» или «эвристиками», не гарантирующими в общем случае нахождения решения (или всех существующих решений). В своей более радикальной формулировке критерий эффективности предполагает отказ даже от логической корректности, т.е. с целью повышения эффективности поисковых процедур возможно построение «быстрых» сверхполных алгоритмов, генерирующих решения, возможно выходящие за рамки логически корректных.

Осмысление этой проблематики привело к возникновению новых теоретических дисциплин. Среди них можно выделить следующие. Во-первых, в рамках вычислительной математики появляется так называемая теория сложности, одним из основных результатов которой было выявление знаменитой P = NP — проблемы и возможных путей ее решения [1]. Несколько огрубляя суть дела, можно сказать, в рамках этой дисциплины исследуется в основном «количественный» (сложностной) аспект проблемы создания эффективных поисковых процедур.

Во-вторых, возможно осмысление проблематики эффективности логических исчислений на более «качественном» уровне, что привело к возникновению в рамках логики нового раздела — теории поиска вывода (ТПВ). К классическим исследованиям этого направления можно отнести работы Д. Пойа [2], Хао Вана [3], С. Кангера [4], С.Ю. Маслова [5], О.Ф. Серебрянникова [6], В.А. Смирнова [7]. Это достаточно молодая область логики, которая, в отличие от логики, не ставит своей задачей (на основе выявления логической формы) исследование правильных способов рассуждений, а акцентирует свое внимание на вопросе «как строить (искать) вывод?». Более точно рамки этого подхода можно определить так. С одной стороны, предпринимается анализ существующих логических исчислений с целью исследования их «эвристического» потенциала и возможностей построения на их базе логических» систем с более эффективными поисковыми процедурами. Т.е. для повышения эффективности поисковых процедур «логическая» составляющая указанных систем должна быть дополнена некоторой «эвристической» составляющей, призванной преодолеть полный перебор при построении вывода. С другой стороны, при построении таких систем хотелось бы не выходить за рамки логически корректными процедур, т.е. наложить на эвристические поисковые процедуры требование не порождать при истинности посылок ложных заключений. Первоначально определенные надежды возлагались на секвенциальные исчисления, в рамках которых возможен «аналитический» подход к построению вывода «снизу вверх»; позже внимание исследователей привлекли системы натурального вывода. Однако вскоре стало ясно, что необходимо переходить к построению нового типа логических исчислений — логико-эвристическим или ин-теллектуальным системам [8].

Помимо этого основного требования к построению «логико-эвристических» систем (требование их логической корректности), выделим еще три существенные идеи, реализованные в рамках проекта.

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