Рассматривается полиномиально-реализуемый класс Delta–формул, интерпретируемый на многосортных моделях с иерархическими надстройками. Структура надстройки описывается произвольной КС-грамматикой. Для теорий из Delta– квазитождеств, обладающих свойством нётеровости и конфлюентности, можно построить константную модель. Предикаты и функции сигнатуры модели интерпретируются на исходном КС-списке, достраиваемом в процессе интерпретации. Этот класс формул можно использовать для моделирования систем реального времени. Приводится пример логической спецификации управляющего устройства поведением робота.
| Файл тезисов: | Глушкова.pdf |