Заключение. 
Исследование и оптимизация условных систем переписывания на основе продукционно-логической модели

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

В дальнейшем можно рассмотреть более общую модель LP-структуры, если в качестве ее основы вместо использовать решетку Линденбаума-Тарского [Расёва и др., 1972]. Тогда моделируемые условные правила смогут в качестве предпосылок и заключений содержать формулы пропозиционального исчисления. При этом общая методология исследования останется прежней.

Интересным представляется переход от равенств термов к модели ориентированных правил и выяснение вопроса о том, как логически эквивалентные преобразования множества правил влияют на основные свойства исходной условной СПТ (нетеровость и конфлюэнтность [Dershowitz et al., 1988], [Klop, 1992]). Можно предположить, что в силу эквивалентности преобразований основные свойства СПТ сохраняются, однако этот вопрос нуждается в формальных исследованиях.