première unification de résolution logique de commande

Question

En supposant que je l'ai montré une partie de la base de connaissances dans le format clausal:

[1] p1(banana).

[2] not p1(X) or p2(Y).
[3] p1(X) or not p3(F).

... et plus de règles.

La plupart des livres, ferait quelque chose comme ceci:

[1,2] {X=banana} p2(Y).

et plusieurs étapes.

Première question: est-il aussi bon de faire quelque chose comme suit:

[2,3] {X=X} p2(Y) or not p3(F).

et puis continuer avec la résolution.

Deuxième question: si différentes variables ont été utilisées dans chaque clause, je pourrais faire la même chose que ci-dessus, par exemple, nous avions:

[2] not p1(X1) or p2(Y1).
[3] p1(X2) or not p3(F2).

[2,3] {X1=X2} p2(Y) or not p3(F2).

Merci d'avance

Answer 1

En supposant $ X $ est une variable ici, plutôt que d'une proposition atomique, alors vous devez d'abord spécifier quelle est la quantification pour 2 et 3. Je suppose qu'il doit être

$ \ forall X, Y \ neg p1 (X) \ Vee p2 (Y) $, et de même pour 3. Dans ce cas, ce qui peut être fait est de remplacer $ X $ et $ Y $ à chaque proposition atomique disponible, afin d'obtenir une base de connaissances propositionnelle, et le travail sur ce point.

Ce que vous proposez à voir avec 2,3 est son que dans la quantification universelle, mais si vous avez seulement la quantification universelle, il est utile en effet.

Pour votre deuxième question: le nom des moyens variables rien, de sorte que votre substitution est son également. En effet, la revendication $ \ forall Y, P (Y) $ est équivalent à $ \ forall Z, P (Z) $. Vous pouvez d'abord changer les noms, si elle vous rend heureux:)

Je remarque que généralement, dans les preuves guidée résolution, il est plus utile pour résoudre une expression concrète d'une règle quantifiée. Par exemple, la résolution de $ P (a) $ avec $ \ forall X P (X) \ Q (X) $ pour obtenir Q $ (a) $. Il est plus probable (heuristically) pour vous aider à la preuve d'une réclamation.