Предваренная нормальная форма
Стандартная форма Скулема
Стандартная форма Скулема
Алгоритм сведения формул исчисления предикатов к предложениям
1)элиминируем импликацию, заменяя ее на дизъюнкцию с отрицанием первого операнда,
2)протаскиваем отрицания по правилам де Моргана к атомам,
3)разделяем связанные переменные так, чтобы они случайно не совпадали в разных кванторах,
4)элиминируем кванторы существования с помощью сколемизации, вводя новые функциональные символы и константы,
5)приводим к предваренной форме, когда у нас формула выглядит так: кванторная приставка и матрица, не содержащая кванторов,
6)элиминируем кванторы всеобщности, поскольку рассматриваем только замкнутые формулы,
7)приводим к конъюнктивной нормальной форме (то есть главной операцией является конъюнкция, и она соединяет группы дизъюнкций),
8)рассыпаем всю формулу на множество предложений, каждое предложение является бескванторной дизъюнкцией литералов.
Пример
