Тождественные преобразования формул

Формулы логики предикатов часто представляют в стандартной форме, например, в клаузальной. Формула в клаузальной форме (в виде конъюнкции – КНФ-дизъюнктов) явно использует лишь операции дизъюнкции, конъюнкции и инверсии, а каждый дизъюнкт – лишь операцию дизъюнкции и инверсии, причем инверсия применяется не более чем к одной предикатной букве (литере, литералу). Поэтому для представления произвольной формулы в форме дизъюнкта необходимо исключить все остальные логические операторы (включая кванторы) и уменьшить область действия знака отрицания до одной предикатной буквы [29].

Исключение знаков импликации.

Знаки импликации исключают, используя равносильность .

Например:

.