Engineering : Steps involved in resolution refutation proofs : Fido is a dog, All dogs are animals, All animals will die, prove that “Fido will die”

To prove the statement “Fido will die” using resolution refutation, we need to follow these steps:

1. Convert the given facts into clauses:
   • Fido is a dog -> Clause 1: Dog(Fido)
   • All dogs are animals -> Clause 2: Animal(x) -> Dog(x)
   • All animals will die -> Clause 3: Animal(x) -> Die(x)
2. Negate the statement to be proved:
   • Negation of “Fido will die” -> ¬Die(Fido)
3. Convert the negated statement into clause form:
   • Negated statement -> Clause 4: ¬Die(Fido)
4. Combine all the clauses:
   • Clauses 1, 2, 3, and 4: {Dog(Fido), Animal(x) -> Dog(x), Animal(x) -> Die(x), ¬Die(Fido)}
5. Apply resolution steps:
   • Select two clauses that contain complementary literals (one positive and one negative) and perform resolution to generate a new clause.
   • Repeat the resolution step until a contradiction (empty clause) is derived or no new clauses can be generated.

Let’s go through the resolution steps for the given set of clauses:

1. Resolve Clauses 1 and 2 using x as a substitution:
   • Resolvent: Animal(Fido)
2. Resolve the resolvent from Step 1 with Clause 3 using x as a substitution:
   • Resolvent: Die(Fido)
3. Resolve the resolvent from Step 2 with Clause 4 using Fido as a substitution:
   • Resolvent: Empty clause (contradiction)

Since we have derived an empty clause (contradiction), we can conclude that the statement “Fido will die” is true based on the given facts and resolution refutation.

In summary, the resolution refutation proof shows that “Fido will die” can be derived from the given facts using resolution steps.