Статья 338

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