Поиск доказательств в натуральном интуиционистском исчислении преди

В.А. Смирнов
Поиск доказательств в натуральном интуиционистском исчислении предикатов.
Предлагается формулировка интуиционистского исчисления предикатов в виде системы субординатного натурального вывода с прямым правилом удаления квантора существования, которое предполагает использование e-термов. На правила введения квантора существования и удаления квантора общности накладывается ограничение непустоты исключаемого (вводимого) терма. С этой целью в язык добавлятся предикат существования. Для предложенного исчисления формулируется система синтетических и аналитических правил поиска вывода, позволяющая алгоритмизировать данную процедуру.

на русском

на английском