"vertexlabeling" - 1 õppematerjal

Experimenting with predicate provers.

solution: p(f(X)) | p(X) ~p(X) | p(f(X)) p(f(X)) | p(f(X)) // resolution p(f(X)) // factoring ~p(X) | ~p(f(X)) p(f(X)) empty clause // resolution applied 2 times Task 7 Draw the failure tree for the following set of clauses: S = { p(f(X)) | q(Y), ~p(X) | q(dog), p(f(dog)) | ~q(X), ~p(f(Z)) } solution: TreePlot[{"p(f(X)) | q(Y)" -> "q(Y)", "~p(f(Z))" -> "q(Y)", "p(f(dog)) | ~q(X)" -> "~q(X)", "~p(f(Z))" -> "~q(X)", "~q(X)" -> "False", "q(Y)" -> "False"}, Top, VertexLabeling -> True] Task 8 Show the execution of the ANL loop to derive the empty clause from: S = { ~r(Y) | ~p(Y), p(b), r(a), p(S) | ~p(b) | ~r(S), r(c) } Use any selection strategy you want, and number the chosen clause at each iteration. 1st ply ~r(Y) | ~p(Y) + p(b) = ~r(Y) ~r(Y) | ~p(Y) + r(a) = ~p(Y) ~r(Y) | ~p(Y) + p(S) | ~p(b) | ~r(S) = ~r(Y) | ~p(b) | ~r(S) = ~r(Y) | ~p(b) = ~r(S) | ~p(b) ~r(Y) | ~p(Y) + r(c) = ~p(Y) p(S) | ~p(b) | ~r(S) + p(b)