Полиномиальная эквивалентность задач изоморфизм предикатных формул и изоморфизм графов

Аннотация

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