В чем заключается алгоритм решения логических уравнений с кванторами всеобщности и существования?

Возможно, имелся в виду алгоритм устранения кванторов существования при решении логических формул с кванторами всеобщности и существования. 12

Алгоритм состоит из нескольких шагов: 1

1. Переименовать связанные переменные так, чтобы ни одна переменная не входила в формулу одновременно связанно и свободно. 1
2. Вынести кванторы в начало формулы, используя эквивалентности. 1
3. Провести сколемизацию, то есть элиминировать в формуле кванторы существования. 1 Для этого для каждого квантора существования выполнить следующий алгоритм: 1

• Если устраняемый квантор существования — самый левый квантор в префиксе формулы, заменить все вхождения в формулу переменной, связанной этим квантором, на новую константу и вычеркнуть квантор из префикса формулы. 1
• Если левее этого квантора существования имеются кванторы всеобщности, заменить все вхождения в формулу переменной, связанной этим квантором, на новый функциональный символ от переменных, которые связаны левее стоящими кванторами всеобщности, и вычеркнуть квантор из префикса формулы. 1

1. Элиминировать кванторы всеобщности. 1 Полученная формула будет бескванторной и эквивалентной исходной в смысле выполнимости. 1
2. Привести формулу к конъюнктивной нормальной форме, для чего воспользоваться эквивалентностями, выражающими дистрибутивность. 1

Если формула содержит свободные переменные, то есть не связанные кванторами всеобщности или существования, то вычислить логическое значение такой формулы нельзя. 2