Задача №6.

Методом резолюций проверить, противоречиво ли множество предложений {f₁, f₂}. Если множество непротиворечиво, то построить модель этого множества.

f₁=$x" y$z" u (P₁(x)Ù ((P₂(x, y)®Ø P₃(y, z))Ú Ø (P₁(z)®P₃(z, u)))),

f₂=" x (P₁(x)®$y (P₂(x, y)Ù Ø P₃(x, y))).

Решение:

f₁= $x" y$z" u (P₁(x)Ù ((P₂(x, y)®Ø P₃(y, z))Ú Ø (P₁(z)®P₃(z, u)))) ~

~$x" y$z" u (P₁(x)Ù ((P₂(x, y)®Ø P₃(y, z))Ú (P₁(z)Ù Ø P₃(z, u)))) ~

~$x" y$z" u (P₁(x)Ù (P₁(z)Ú Ø P₂(x, y)Ú Ø P₃(y, z))Ù (Ø P₂(x, y)Ú Ø P₃(y, z)).

f₂= " x (P₁(x, y)®$y (P₂(x, y)Ù Ø P₃(x, y))) ~

~" x(Ø P₁(x)Ú $y (P₂(x, y)Ù Ø P₃(x, y))) ~

~" x$y((Ø P₁(x)Ú P₂(x, y)Ù (Ø P₁(x)Ú Ø P₃(x, y))).

(1)P₁(x) (2)P₁(z)Ú Ø P₂(x, y)Ú Ø P₃(y, z) (3)Ø P₂(x, y)Ú Ø P₃(y, z) (4)Ø P₁(x)Ú P₂(x, y) (5)Ø P₁(x)Ú Ø P₃(x, y)

Строим модель: S=< P , P , P >

res((1), (4)) = P₂(x, z) - (6)

res((6), (3)) = Ø P₃(y, z)

Ø P₃(y, z) = 0 Þ P₃(y, z) = 1