Resolution refutation question confused

Question

I'm trying to solve this problem for my class. But now I'm so confused about the following question.

*Consider the following statements:

1. Every boy or girl is a child.
2. Every child gets a doll or a train or a lump of coal.
3. No boy gets a doll.
4. No child who is good gets a lump of coal.

a. Use the predicates BOY, GIRL, CHILD, GET-DOLL, GET-TRAIN, GET-COAL and GOOD to represent these statements as predicate calculus formulas.

b. Convert these statements to clauses.

c. Use resolution refutation to prove that if no child gets a train, then no boy is good.*

after first two-step, I can't prove the conclusion. One reason I think is that there is a girl function in the first clause, so I can't get an empty clause finally. The second reason is that I'm not sure whether I can use a clause many times to do the resolution refutation. Other similar questions are easy to prove by just using clause once and join them together, finally, I can get NIL or empty clause. But I can't prove this one. I don't know how to do.

The working step 01

The working step 02(Please ignore this, I think the goal is wrong in this image

==============

Goal and resolution refutation - 1(New version)

Goal and resolution refutation - 2(New version)

Answer 1

In formal logic I believe you can use a statement as many times as you like so long as it's derived or assumed (taken as an axiom) so if you have a statement at your disposal, you should be able to use it as many times as you like. You need to think about what it means to negate a statement.

I believe you will need to create a formula for each of the 4 statements listed and join them with an AND connective. From what I just read on resolution refutation you should just need to cancel out conflicting terms as they appear.

I hope this helps.

Answer 2

Your goal is still not good. You treat the goal as being just one big universal statement, but the goal is a conditional between two universal statements:

$$\forall x_5 (CHILD(x_5) \to \neg GET-TRAIN(x_5)) \to \forall x_6 (BOY(x_6) \to \neg GOOD(x_6))$$

Negating that, you get:

$$\forall x_5 (CHILD(x_5) \to \neg GET-TRAIN(x_5)) \land \neg \forall x_6 (BOY(x_6) \to \neg GOOD(x_6))$$

And thus both:

$$\forall x_5 (CHILD(x_5) \to \neg GET-TRAIN(x_5))$$

and

$$\neg \forall x_6 (BOY(x_6) \to \neg GOOD(x_6))$$

the first one is easily clausified:

$$\neg CHILD(x_5) \lor \neg GET-TRAIN(x_5)$$

but for the second one you get:

$$\exists x_6 (BOY(x_6) \land GOOD(x_6))$$

Now, do you know what to do with an existential?