Computer science work

1. Run the attached marriage problem (java -jar Marriage.jar) and either find a perfect family or a social club for each of the eight towns. Attach your log file to your answers.

2. Run the attached Logic program (java -jar Logic.jar) and find proofs for the following theorems:

• 1.3 #2b

• 1.4 #2f

• 1.4 #2j

• 1.6 #3a

• 1.6 #3c

To prove a theorem, say 1.3 #2b, choose "File -> Select -> Chapter 1 -> Exercises 1.3 -> 2 -> b" from the menu. To create a box, choose "Open" from Rules menu. To end a box, choose "Close" from the Rules menu. Be careful when clicking on the justification lines that you do so in the same order as given on the rule sheet. Save your proof to a file and attach it to your answers. One hint: You may have to use the law of the excluded middle (P v ~P for some P). It's in the derived rules section under the rules menu.

3. (Research Question): Compare and contrast three state-of-the-art theorem provers. Are they specialized to any particular areas? What methods to they use? State your references.

4. Translate the following word problem into predicate calculus:

Every person is either a witch or a mortal, but never both. Witches love everyone who loves them. Glinda is a witch in love. A mortal will only love a witch who does not love any mortal. Therefore, either some witch loves Glinda, or some mortal does not love Glinda.

5. Prove that the conclusion of the above problem follows from the hypotheses using a resolution theorem prover, for example, you may use Prover9. To use Prover9, log in to any of the Math/CS classroom or lab machines on the Linux side using your Math/CS account, and type '/program/prover/prover9 < myfile.in' where 'myfile.in' contains your theorem.) See Prover9 documentation for details on using Prover9.

6. Give the most general unifier (MGU) for each of the following sets of clauses, or say 'None' if the set does not have a unifier. Assume that r, s, u, v, w, x, y, and z are the variables.

• { P(x,y,z), P(f(w),v,v), P(f(g(r)),r,s) }

• { P(x,y), ~P(y,x) }

• { loves(x, father(x)), loves(Bob, y) }

• { lessThan(x, plus(x,1)), lessThan(2, y), lessThan(z, 3) }

• { Q(x,y,z,w), Q(u,u,v,v), Q(r,s,r,s) }