Аннотация доклада.

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

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