Logic for Computer Science:

Given the following set of facts: 1. All dogs howl at night. 2. Anyone who has any cats will not have any mice. 3. Light sleepers do not have anything which howls at night. 4. Peter has either a cat or a dog. Prove by resolution refutation in FOL that if Peter is a light sleeper, then Peter does not have any mice.

Note: To model this problem, please use the following predicates: DOG(x): x is a dog CAT(x): x is a cat MOUSE(x): x is a mouse HOWL(x): x howls at night HAVE(x,y): x has y LS(x): x is a light sleeper