Зарипова, Э.Р. Дискретная математика Часть II. Математическая логика

63 F G F G F G F G       или ( ) [ ] ( ) [ ] ( ) [ ] ( ) [ ], x F x x F x x F x x F x       чтобы внести знак отрицания внутрь формулы. Шаг 3. Переименовываем связанные переменные, если это необходимо. Шаг 4. Используем эквивалентности (12.1) - (12.6), (12.11), (12.12). Пример 12.1. Привести к предваренной нормальной форме формулу (  x)P(x)  (  x)Q(x). ( ) ( ) ( ) ( ) ( )( ( ) ( )) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) x P x x Q x x P x Q x x P x x Q x x Q x x P x                Пример 12.2. Привести к предваренной нормальной форме формулу (  x) (  y)(((  z)P(x,z)  P(y,z))  (  u)Q(x,y,u)). ( )( )((( ) ( , ) ( , )) ( ) ( , , )) ( )( )((( ) ( , ) ( , )) ( ) ( , , )) ( )( )((( )( ( , ) ( , )) ( ) ( , , )) ( )( )( )( )( ( , ) ( , ) ( , , )). x y z P x z P y z u Q x y u x y z P x z P y z u Q x y u x y z P x z P y z u Q x y u x y z u P x z P y z Q x y u                            13. Скулемовская стандартная форма. Подстановка и унификация. Алгоритм унификации Скулемовская стандартная форма