Статья 353

Повышение, выразительной силы и аккуратности выводов в интуиционистской логике по сравнению с классической имеет и оборотную сторону поиск вывода в ней существенно сложнее. В частности, метод резолюций не может применяться потому, что формулы не могут быть разложены на дизъюнкты.
Интуиционистская логика хорошо подходит для описания задач, в которых требуется вычислить новые величины по заданным величинам и вспомогательным функциям и ни один из вычисленных ресурсов время, память, надежность не налагает суровых ограничений.
Для других ситуаций интуиционистскую логику приходится варьировать. Например, если ограничения по памяти существенны, можно использовать логику Ж.-И. Жирара, если вычисления не найдены - симметрическую конструктивную логику, развитую, в частности, Н. Заславским, который использовал идеи Р. Нельсона и А.А. Маркова.

Логика как инструмент анализа, понятий программирования.