Answers.Body: <p>Hey I am currently studying First Order Logic right now and I think I can answer your question. Others please correct me if I am wrong. </p>
  
  <p>For the first case, you can generally substitute variables with constants. Hence, you can make the substitution <span class="math-container">$\theta \leftarrow \{x_1 \leftarrow A, y_1 \leftarrow B \}$</span>. This is used very commonly when you want to infer some query <span class="math-container">$\alpha$</span> from your knowledge base. <span class="math-container">$\alpha$</span> usually is in the form <span class="math-container">$P(A,B)$</span> as you have mentioned. When you unify you get <span class="math-container">$\neg L(A) \vee H(A)$</span> and ur substitution has to stay the same throughout the resolution algorithm. I.e, you cannot substitute <span class="math-container">$x_1$</span> for another constant / variable. </p>
  
  <p>Regarding the second case, you cannot substitute a constant with a variable <span class="math-container">$B$</span> to another variable. </p>
  
  <p>In general, you can substitute a variable with a constant, or another variable. You can also substitute a variable with a skolem function, Eg. <span class="math-container">$x_1 \leftarrow G(y)$</span>. However, for skolem functions, you cannot substitute <span class="math-container">$x \leftarrow F(x)$</span>, in which the variable names are the same. </p>
  
  <p>Hope this helps ! </p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-04-30T07:30:41.150Z
Answers.LastActivityDate: 2020-04-30T07:30:41.150Z
Answers.UserDisplayName: calveeen
Body: <p>I'm checking out how to manually apply resolution on a first order predicate logic knowledge base and I'm confused about what is allowed or not in the algorithm.</p>
  
  <p>Let's say that we have the following two clauses (where <span class="math-container">$A$</span> and <span class="math-container">$B$</span> are constants):</p>
  
  <p><span class="math-container">$\neg P(A, B) \vee H(A)$</span></p>
  
  <p><span class="math-container">$\neg L(x_1) \vee P(x_1, y_1)$</span></p>
  
  <p>If I try to unify these two clauses by making the substitutions <span class="math-container">$\{x_1/A, y_1/B\}$</span> do I get <span class="math-container">$\neg L(A) \vee H(A)$</span> ? Is it allowed to substitute <span class="math-container">$y_1$</span> by <span class="math-container">$B$</span> even if <span class="math-container">$B$</span> doesn't appear in the unified clause?</p>
  
  <p>Then we have the other way around where:</p>
  
  <p><span class="math-container">$\neg P(A, y_1) \vee H(A)$</span></p>
  
  <p><span class="math-container">$\neg L(x_1) \vee P(x_1, B)$</span></p>
  
  <p>Can I do <span class="math-container">$\{x_1/A, B/y_1\}$</span> for <span class="math-container">$\neg L(A) \vee H(A)$</span> ?</p>
  
  <p>What about the case where:</p>
  
  <p><span class="math-container">$\neg P(A, z_1) \vee H(A)$</span></p>
  
  <p><span class="math-container">$\neg L(x_1) \vee P(x_1, y_1)$</span></p>
  
  <p>Can I substitute <span class="math-container">$\{x_1/A, y_1/z_1\}$</span> and get <span class="math-container">$\neg L(A) \vee H(A)$</span> ?</p>
  
  <p>Finally there is also the cases where we have something like this:</p>
  
  <p><span class="math-container">$\neg P(x_2, y_2) \vee H(z_1)$</span></p>
  
  <p><span class="math-container">$\neg L(x_1) \vee P(x_1, y_1)$</span></p>
  
  <p>Can we do <span class="math-container">$\{x_1/x_2, y_1/y_2\}$</span> to get <span class="math-container">$\neg L(x_3) \vee H(z_2)$</span> ?</p>
  
  <p>I'm really confused about when unification succeeds once we have two clauses with a literal of the same kind (negation in one of them and not in the other one) that are a candidates for unification. </p>
  
Tags: <logic>
Title: Does the substituted variable/constant have to appear in the unified term?
UserDisplayName: nsa
ThreadText: # Does the substituted variable/constant have to appear in the unified term?
  
  (Asked by: username_0 on 2019-11-30)
  
  I'm checking out how to manually apply resolution on a first order predicate logic knowledge base and I'm confused about what is allowed or not in the algorithm.
  
  Let's say that we have the following two clauses (where $A$ and $B$ are constants):
  
  $\neg P(A, B) \vee H(A)$
  
  $\neg L(x\_1) \vee P(x\_1, y\_1)$
  
  If I try to unify these two clauses by making the substitutions $\{x\_1/A, y\_1/B\}$ do I get $\neg L(A) \vee H(A)$ ? Is it allowed to substitute $y\_1$ by $B$ even if $B$ doesn't appear in the unified clause?
  
  Then we have the other way around where:
  
  $\neg P(A, y\_1) \vee H(A)$
  
  $\neg L(x\_1) \vee P(x\_1, B)$
  
  Can I do $\{x\_1/A, B/y\_1\}$ for $\neg L(A) \vee H(A)$ ?
  
  What about the case where:
  
  $\neg P(A, z\_1) \vee H(A)$
  
  $\neg L(x\_1) \vee P(x\_1, y\_1)$
  
  Can I substitute $\{x\_1/A, y\_1/z\_1\}$ and get $\neg L(A) \vee H(A)$ ?
  
  Finally there is also the cases where we have something like this:
  
  $\neg P(x\_2, y\_2) \vee H(z\_1)$
  
  $\neg L(x\_1) \vee P(x\_1, y\_1)$
  
  Can we do $\{x\_1/x\_2, y\_1/y\_2\}$ to get $\neg L(x\_3) \vee H(z\_2)$ ?
  
  I'm really confused about when unification succeeds once we have two clauses with a literal of the same kind (negation in one of them and not in the other one) that are a candidates for unification.
  
  **Tags:** logic
  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_1 on 2020-04-30. Score: 0
  
  Hey I am currently studying First Order Logic right now and I think I can answer your question. Others please correct me if I am wrong.
  
  For the first case, you can generally substitute variables with constants. Hence, you can make the substitution $\theta \leftarrow \{x\_1 \leftarrow A, y\_1 \leftarrow B \}$. This is used very commonly when you want to infer some query $\alpha$ from your knowledge base. $\alpha$ usually is in the form $P(A,B)$ as you have mentioned. When you unify you get $\neg L(A) \vee H(A)$ and ur substitution has to stay the same throughout the resolution algorithm. I.e, you cannot substitute $x\_1$ for another constant / variable.
  
  Regarding the second case, you cannot substitute a constant with a variable $B$ to another variable.
  
  In general, you can substitute a variable with a constant, or another variable. You can also substitute a variable with a skolem function, Eg. $x\_1 \leftarrow G(y)$. However, for skolem functions, you cannot substitute $x \leftarrow F(x)$, in which the variable names are the same.
  
  Hope this helps !
  
  
  ---
  
  