Исследовательская группа
Лаборатория языковых инструментов
Ленивый синтез функций по спецификациям первого порядка
February 25
В докладе будет рассказано о недавно предложенном подходе к синтезу нерекурсивных функций по спецификациям, написанным в виде ∀∃-формул первого порядка. Метод основан на ленивом устранении кванторов через последовательное вычисление проекций на основе моделей спецификации и позволяет эффективно синтезировать функции с более чем одним выходом.
Материалы к докладу:
Докладчик: Дмитрий Мордвинов