Семантическое программирование и полиномиально вычислимые представления

В работе исследуются вопросы существования полиномиально вычислимых представлений для базовых синтаксических конструкций логики предикатов первого порядка, а также для объектов семантического программирования таких как L-программы и L-формулы. Было показано, что множество доказательств (как линейных, так и в виде дерева) в исчислении предикатов первого порядка имеют полиномиально вычислимые представления. Также получен ряд утверждений, которые помогают более эффективно доказывать полиномиальность: обобщенная PAG-теорема с полиномиально вычислимыми начальными условиями, а также утверждение о p-итерационных термах с ослабленными оценками. Данная работа может быть полезна для построения логических языков программирования, смарт контрактов, а также построения быстрых алгоритмов автоматической проверки доказательств.