CS 244/444

Exercise Set 2: Resolution Proofs - Hardcopy due in class Thursday Oct 7

1. Represent the following situation in propositional logic: The suspects in a robbery are Anne, Betty, and Chloe. Exactly one of the suspects is guilty. When questioned, a guilty suspect might lie or tell the truth, but an innocent one always tells the truth. Anne tells the police that Betty is innocent. Betty tells them that she was out of town the day the robbery occurred. Chloe says that Betty was in town the day of the robbery. If a suspect is out of town the day of the robbery, then she must be innocent. Create a resolution refutation proof that Chloe is guilty.

Note that you can represent the guilt of each suspect by a proposition (e.g., A means "Anne is guilty", B means "Betty is guilty", etc.). Since non-guilty suspects tell the truth, their testimony can be represented by implications, for example, "Anne tells the police that Betty is innocent" can be represented as ~A => ~B.

2. Rewrite the situation using first-order logic and the predicates Guilty(x) and OutOfTown(x). Create a FOL resolution proof using answer extraction to determine who the guilty person is. Note that in this case you do NOT assert that Chloe is not guilty and find a contradiction! Instead, you assert [~Guilty(x) v Answer(x)], and create a proof that derives [Answer(PERSON)] where PERSON is the name of the guilty person.

3. This disease sickle cell anemia is carried by a recessive gene. The symptoms of the disease appear if a person inherits the gene from both parents. We can represent this as follows:

A person with the gene for sickle cell anemia is either someone who exhibits the disease or is a carrier.

All x . G(x) <=> (A(x) v C(x))

If a person exhibits the disease, then both the mother and father must have had the gene.

All x . A(x) => (G(mother(x)) & G(father(x)))

If a person is a carrier, then at least one of the mother and father must have had the gene.

All x . C(x) => (G(mother(x)) v G(father(x)))

Create a FOL resolution proof that if a person has the disease, then either their paternal grandmother or paternal grandfather has the gene; that is, prove:

All x . A(x) => (G(mother(father(x)) v G(father(father(x))))

4. (This problem is for students taking this class as CSC 444 only.) Formalize the following (somewhat fanciful) statements about chemistry in FOL and provide a resolution refutation proof of the specified theorem. Assume that domain of all the variables is the set of elements, you do not need to use an explicit predicate to assert that something is an element.

1. The elements are divided into metals, metaloid, non-metals, and inert gases. (Note that these are non-overlapping groups. In particular, non-metals does NOT mean everything that is not a metal!)
2. A metal that reacts with all non-metals is a super-metal.
3. Anything that is not an inert gas reacts with Hydrogen.
4. Hydrogen is a metal.
5. Prove: Hydrogen is a super-metal.

Depending upon how you wrote your clauses, you may need to include the assertion that the relationship ReactsWith is reflexive in your axioms in order to prove the theorem.