УДК 512.563.6 АЛГЕБРАИЧЕСКАЯ ИНТЕРПРЕТАЦИЯ УСЛОВНЫХ СИСТЕМ ПЕРЕПИСЫВАНИЯ НА ОСНОВЕ LP-СТРУКТУР Д. В. <...> Теория систем переписывания представляет эффективный аппарат для решения ряда важных задач искусственного интеллекта и компьютерной алгебры. <...> В статье вводится алгебраическая система c семантикой совокупности правил условной эквациональной теории или условной системы переписывания термов. <...> Для данной модели рассматриваются следующие основные вопросы: замкнутость, эквивалентные преобразования, структура замыкания, логическая редукция. <...> Полученные результаты могут быть применены для исследования и автоматической оптимизации соответствующего множества правил. <...> ВВЕДЕНИЕ Системы переписывания термов (СПТ) находят применения при решении таких известных задач как автоматическое доказательство теорем [1], символьное упрощение алгебраических выражений [2], верификация компьютерных программ [3] и ряда других. <...> Важными вопросами, связанными с СПТ, являются эквивалентные преобразования и упрощение их множеств правил. <...> В то время как для обычных СПТ подобные задачи решались в ряде работ (например, [4]), для условных СПТ они еще остаются открытыми. <...> Данное обстоятельство объясняется более сложной структурой правил условных СПТ. <...> Для обычных систем задача минимизации множества правил сводится к транзитивной редукции некоторого бинарного отношения («элиминация транзитивности»). <...> При определении системы переписывания отправной точкой является эквациональная теория, множество правил которой состоит из равенств термов. <...> Поскольку обычно именно эквациональная теория дает критерий эквивалентности систем переписывания, исследование в этом плане условных СПТ может быть начато с рассмотрения эквивалентности самих условных эквациональных теорий. <...> Полученные результаты, в частности, впервые решают задачу построения логической редукции условной эквациональной теории. <...> Однако рассмотренная в [7] алгебраическая <...>