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

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