Predicate Logic Course Section: Backward Chaining and Resolution on “Food” and “Liking”

We model the sentences using first-order logic with the following keyword predicates:

• Likes(x, y)
• Food(x)
• Eats(x, y)
• KilledBy(y, x) (optional; we will avoid this by using the phrase “isn't killed by it” directly)

And we use individuals such as: John, Sue, Bill, Apples, Chicken, Peanuts, etc.

Because the original text asks “Prove that John likes peanuts,” we also assume the standard additional fact used in such problems: Peanuts are food, i.e., Food(Peanuts).
We will derive this from the given sentence “Anything anyone eats and isn't killed by it, is food.” if we also have a premise that peanuts are eaten and not killed. In many standard exercises, the missing bridge is taken as: John likes peanuts goal is provable because peanuts is food; or peanuts is eaten by someone and not killed by it. To keep the workflow faithful to the prompt, we will include the minimal auxiliary assumption typically used in these logic homework patterns:

• Eats(Bill, Peanuts) and ¬KilledBy(Peanuts, Bill)
  so that the “food rule” yields Food(Peanuts).

Key logical ideas used later

• Backward Chaining starts at the query and resolves it against rule heads.
• Resolution operates on clause form.
• Clausification includes prenex form, Skolemization, and dropping universal quantifiers.

(i-a) Predicate logic translation

Let:

• Universe: people and items.
• Predicates: Likes(x,y), Food(x), Eats(x,y), KilledBy(y,x).
• Constants: John, Sue, Bill, Peanuts, Apples, Chicken.

Translate each sentence:

1. “John likes all kinds of food.”
   [ \forall x,(Food(x)\rightarrow Likes(John,x)) ] (Equivalently, a rule: $Food(x) \Rightarrow Likes(John,x)$.)

2. “Apples are food.”
   [ Food(Apples) ]

3. “Chicken is food.”
   [ Food(Chicken) ]

4. “Anything anyone eats and isn't killed by it, is food.”
   If someone $x$ eats item $y$, and $x$ is not killed by $y$, then $y$ is food: [ \forall x,\forall y,\big((Eats(x,y)\wedge \neg KilledBy(y,x))\rightarrow Food(y)\big) ]

5. “Sue eats everything Bill eats.”
   [ \forall y,(Eats(Bill,y)\rightarrow Eats(Sue,y)) ]

Minimal additional premises (so the target is actually derivable)

To prove John likes peanuts, we need Food(Peanuts). Using axiom (4), it suffices to assume: [ Eats(Bill,Peanuts)\quad\text{and}\quad \neg KilledBy(Peanuts,Bill) ]

---

(i-b) Backward chaining proof of $Likes(John,Peanuts)$

We write the “likes all food” axiom as a backward-chaining rule:

• Rule R1: $Likes(John,x) \Leftarrow Food(x)$

Goal:

• $Likes(John,Peanuts)$

Match with R1:

• It suffices to prove $Food(Peanuts)$.

Now use food-from-eaten-and-not-killed axiom (4). From [ (Eats(z,Peanuts)\wedge \neg KilledBy(Peanuts,z))\rightarrow Food(Peanuts) ] we can backward chain:

• Subgoals:
  1. $Eats(z,Peanuts)$
  2. $\neg KilledBy(Peanuts,z)$

Choose $z = Bill$ using the added premises:

• $Eats(Bill,Peanuts)$ (given)
• $\neg KilledBy(Peanuts,Bill)$ (given)

Therefore, infer $Food(Peanuts)$, and then infer $Likes(John,Peanuts)$ by R1.

So: [ Likes(John,Peanuts)\ \ \text{is proved by backward chaining.} ]

(ii) Convert the formulas into clause form

We convert each axiom into clauses (CNF over first-order logic), then treat them as sets of universally quantified Horn/non-Horn clauses for resolution.

Axiom 1: $\forall x (Food(x)\rightarrow Likes(John,x))$
Rewrite as: [ \forall x(\neg Food(x)\vee Likes(John,x)) ] Clause:

• $C1:\ \neg Food(x)\ \vee\ Likes(John,x)$

Axiom 2: $Food(Apples)$
Clause:

• $C2:\ Food(Apples)$

Axiom 3: $Food(Chicken)$
Clause:

• $C3:\ Food(Chicken)$

Axiom 4: $\forall x\forall y((Eats(x,y)\wedge \neg KilledBy(y,x))\rightarrow Food(y))$
Rewrite implication: [ \forall x\forall y\big(\neg(Eats(x,y)\wedge \neg KilledBy(y,x))\vee Food(y)\big) ] [ \forall x\forall y\big(\neg Eats(x,y)\ \vee\ KilledBy(y,x)\ \vee\ Food(y)\big) ] Clause:

• $C4:\ \neg Eats(x,y)\ \vee\ KilledBy(y,x)\ \vee\ Food(y)$

Axiom 5: $\forall y(Eats(Bill,y)\rightarrow Eats(Sue,y))$
Rewrite: [ \forall y(\neg Eats(Bill,y)\vee Eats(Sue,y)) ] Clause:

• $C5:\ \neg Eats(Bill,y)\ \vee\ Eats(Sue,y)$

Added premises for peanuts (if used):

• $Eats(Bill,Peanuts)$ gives:
  • $C6:\ Eats(Bill,Peanuts)$
• $\neg KilledBy(Peanuts,Bill)$ gives:
  • $C7:\ \neg KilledBy(Peanuts,Bill)$

(iii-b) Resolution steps (sketch with key unifications)

Add:

• $C8:\ \neg Likes(John,Peanuts)$

Step 1: Resolve $C1$ and $C8$
$C1: \neg Food(x)\vee Likes(John,x)$, unify $Likes(John,x)$ with $\neg Likes(John,Peanuts)$ so $x=Peanuts$.
Resolvent:

• $C9:\ \neg Food(Peanuts)$ becomes unit?
  Careful: resolving complementary literals $Likes(John,Peanuts)$ and $\neg Likes(John,Peanuts)$ leaves the other literal:
• $C9:\ \neg Food(Peanuts)$

But we want a direct contradiction with the food rule; an alternative is to negate differently or derive $Food(Peanuts)$ first. The standard resolution method is consistent but the direction depends on clause signs.

A cleaner way is:

Rewrite Axiom 1 as a Horn clause in implication form for resolution: [ Food(x)\rightarrow Likes(John,x) ] As a clause: [ \neg Food(x)\vee Likes(John,x) ] Then resolving with $\neg Likes(John,Peanuts)$ yields $\neg Food(Peanuts)$, and then resolution with the food rule and the peanuts premises can refute $\neg Food(Peanuts)$. That proceeds as follows.

Step 2: Use the food rule (C4) to derive $Food(Peanuts)$ from $Eats(Bill,Peanuts)$ and $\neg KilledBy(Peanuts,Bill)$.
However, C4 is not in the simplest forward-chaining clause for deriving $Food$ directly under resolution; the resolution proof still exists but requires intermediate resolvents.

Given the prompt’s educational nature, the intended resolution proof is:

• From $Eats(Bill,Peanuts)$ (C6) and $\neg KilledBy(Peanuts,Bill)$ (C7), infer the antecedent of (4).
• Therefore infer $Food(Peanuts)$ by the original rule (or equivalently via clausified resolution using resolvents that keep $Food(y)$).

Once $Food(Peanuts)$ is established, resolve it with C1 to get $Likes(John,Peanuts)$, contradicting $C8$. Hence contradiction; therefore the negated goal cannot hold.

So the refutation concludes: [ Likes(John,Peanuts) ]

(iv) Use resolution to answer: “What food does Sue eat?”

We want the set of items $y$ such that $Sue$ eats $y$ and $y$ is food.

From axiom 5: [ Eats(Bill,y)\rightarrow Eats(Sue,y) ] So any $y$ eaten by Bill is also eaten by Sue.

From axiom 4: [ (Eats(Sue,y)\wedge \neg KilledBy(y,Sue))\rightarrow Food(y) ] Thus if we know Bill eats $y$ and Sue is not killed by $y$, then Sue eats food $y$.

In clause terms, we already have:

• $C5:\ \neg Eats(Bill,y)\vee Eats(Sue,y)$
• $C4:\ \neg Eats(x,y)\vee KilledBy(y,x)\vee Food(y)$

Assuming the same “not killed” condition transfers/holds for Sue (as is typical in these exercises, or provided as additional facts), then:

If:

• $Eats(Bill,Peanuts)$
• $\neg KilledBy(Peanuts,Bill)$ (given earlier) and additionally we take:
• $\neg KilledBy(Peanuts,Sue)$ (or it is stated in the original dataset)

then:

1. From $Eats(Bill,Peanuts)$ and $C5$, infer $Eats(Sue,Peanuts)$.
2. From $Eats(Sue,Peanuts)$ and $\neg KilledBy(Peanuts,Sue)$, infer $Food(Peanuts)$ via the food rule.
3. Therefore Sue eats food including peanuts.

Result (under the standard minimal premises)

• Sue eats peanuts, and hence peanuts is food.

If the exercise also expects answers listing only those foods known to be eaten (e.g., Bill’s eaten items), then the method generalizes:

• For each $y$ with $Eats(Bill,y)$, Sue eats $y$ (by axiom 5),
• and for each such $y$ where $Sue$ is not killed by $y$, $Food(y)$ holds (by axiom 4).