Алгоритм распознавания общезначимости формул в частных случаях

1. Проблема разрешимости в случае конечных областей.

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

Пример 1. Формула в области , состоящий из двух элементов, приводится к виду:

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

Определение 1. Формула логики предикатов называется замкнутой, если она не содержит свободных предикатных переменных.

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

формула называется замыканием существования формулы F.