COMP 3190 Assignment 1: Formal Representation and Reasoning.
Due: Friday, February 7, 2020, by 10:30am (electronic handin on D2L – no late assignments – be aware of the deadline and leave time to hand it in). All answers must be typeset using a text editor or word processing program and submitted as a PDF document (other document types will be ignored, you have been warned). Assignments not handed in through D2L (e.g. hand-written or emailed answers) will not be accepted. You must also have agreed to an electronic term honesty declaration on D2L sometime before the assignment is due (you will not be able to see the handin dropbox until you have agreed to the terms of the honesty declaration, so do this early).
There are 66 marks in total (note the original assignment had an incorrect total). Each assignment will be worth proportionally the same value to your overall grade irrespective of the total marks on the assignment.
This assignment involves some exercises in representation – specifically, First Order Logic, Clause Form, Unification, and Resolution Refutation (all of these proofs require resolution refutation: no marks are available for any other form of reasoning). The point of this assignment is to get you thinking about formal representation for problem solving, and the processes involved in reasoning before we start using a computer to do this. Pay attention to the level at which you are representing facts – try to make it so that concepts are general and could be extended.
I realize that doing formal symbols in most typesetting programs is very tedious. To make life a little easier and to be able to use standard text files, you may use the notation forall(X):wff(X) for a universal quantifier, and exists(X):wff(X) for an existential quantifier. ~, ^, v (use the lowercase letter v) and -> can be used directly off the keyboard for not, and, or, and implication.
Question 1. 17 Marks.
Consider the following English statements, which form a logical system. If you do not recognize any of these names, just assume that Los Pollos Hermanos is the name of a restaurant, and the other capitalized items are the names of people.
1. Jesse, Heisenberg, Gale, and Gus are in Los Pollos Hermanos
2. Jesse is not well-dressed and he is also not happy.
3. Heisenberg and Gale like poetry.
4. Gus is a manager and likes seafood.
5. All managers are well-dressed.
6. Anyone who is not happy does not like anything.
7. Everyone in Los Pollos Hermanos who is not a manager and does not like poetry
is a cook.
8. All cooks in Los Pollos Hermanos get free chicken.
9. Some cooks like Saul Goodman.
10. Anyone who likes Saul Goodman gets free chicken.
Convert these statements to first order logic – every numbered statement should result in a single first order logic statement (6 marks). Then convert the statements to clause form (5 marks – you must SHOW YOUR WORK if you want any part marks to be considered) and using resolution refutation, prove that Jesse gets free chicken (6 marks). Each clause form statement should state the number of the original FOL statement that it came from, and each should also be numbered so the marker can follow your reasoning in the resolution proof. Each new resolution should show the two parents clauses used to derive the resolution, along with the necessary substitutions for unification.
Q1 Solution (17 Marks)
The Q1 solution is organized by taking everything statement by statement and putting it into FOL and then clause form individually. You might also have shown the whole system in FOL first and then the whole in clause form (which is how I do the Q2 solution). Either way is fine but it should be clear from context/organization which is being done.
For FOL translation you need to ensure you have all the basic concepts as in my solution below. Things should be modular and that concepts should be set out so that the example could be extended without rewriting a whole lot. There should not be nested concepts – this is not modular and is often the result of being afraid of using predicates with two or more symbols participating. Also watch out for lengthy concepts (well-dressed- manager(x)) or other things that put two concepts together that make more sense separately!), and concepts that you couldn’t possibly use together (e.g. likes vs dislikes, where there’s no logical thing to state that these are inverses). Concepts should also be consistent throughout (manager(X) changing to is-manager(X) isn’t unifiable).
One classic mistake to note is mixing up implies & and: saying forall(X): characteristic(X) ^ othercharacteristic(X) (“everything in the system has characteristic and othercharacteristic” instead of forall(X): characteristic(X) -> conclusion(X) (if an object has characteristic, we can then say it has othercharacteristic too!). there are other classic mistakes to take note of mentioned in the representation notes as well). Similar problems can happen with existentials.
For translation to clause form, you need to make sure you do it fully – if there’s even something as simple an and left you won’t be able to do resolution. I put more brackets in for clarity than you may have, just to make things obvious.
For resolution: You should get NO marks if you haven’t done any resolution refutation – i.e. proving this using anything other than resolution is not worth anything.
======================================================= Jesse, Heisenberg, Gale, and Gus are in Los Pollos Hermanos
pollos(jesse) ^ pollos(heisenberg) ^ pollos(gale) ^ pollos(gus)
You may have done this as a 2-place predicate (in(jesse,pollos)) too, and that’s fine You Can’t have one huge in() predicate with all the people as arguments, it doesn’t work that way.. The question does say one FOL statement per English statement, so you do need the ands here. Now split to clause form:
1) pollos(jesse)
2) pollos(heisenberg) 3) pollos(gale)
4) pollos(gus)
Jesse is not well-dressed and he is also not happy.
~welldressed(jesse) ^ ~happy(jesse)
could also be dressed(jesse,well) if you wanted to be more general and be able to refer to other kinds of dress, but you don’t actually need that.
clause form – split to 5) ~welldressed(jesse) 6) ~happy(jesse)
Heisenberg and Gale like poetry (should be 2-place predicate – different uses of likes) likes(heisenberg, poetry) ^ likes(gale,poetry) now split these to get clause form
7) likes(heisenberg, poetry)
8) likes(gale, poetry)
Gus is a manager and likes seafood
manager(gus) ^ likes(gus, seafood) again, 2-place – now split these to get clause form 9) manager(gus)
10) likes(gus, seafood)
All managers are well-dressed.
forall(X): manager(X)-> welldressed(X)
need to remove implication, then quantifier for clause form: forall(X): ~manager(X) v welldressed(X)
11) ~manager(X) v welldressed(X)
Anyone who is not happy does not like anything.
forall(Y,Z): ~happy(Y) -> ~likes(Y,Z). forall(z) Could also be after implies, but then it would have to be shifted over during conversion.
remove implication
forall(Y,Z): ~(~happy(Y)) v ~likes(Y,Z)
forall(Y,Z): happy(Y) v ~likes(Y,Z)
remove quantifier
12) happy(Y) v ~likes(Y,Z)
I’m standardizing variables apart by picking a new variable name each time, it takes less space than doing it at the end…but it could be done at the end too.
Everyone in Los Pollos Hermanos who is not a manager and does not like poetry is a cook.
forall(Q): (pollos(Q) ^ ~manager(Q) ^ ~likes(Q, poetry)) -> cook(Q)
Remove the implication
forall(Q): ~(pollos(Q) ^ ~manager(Q) ^ ~likes(Q, poetry)) v cook(Q)
move negation in
forall(Q): ~pollos(Q) v manager(Q) v likes(Q, poetry) v cook(Q)
remove quantifier:
13) ~pollos(Q) v manager(Q) v likes(Q, poetry) v cook(Q)
All cooks in Los Pollos Hermanos get free chicken.
forall(R): (pollos(R) ^ cook(R)) -> gets-free(R, chicken)
I tried to make getting something free general, but gets-free-chicken, or adding free as third participant in the predicate (cost) are both ok. Now, get rid of implication: forall(R): ~(pollos(R) ^ cook(R)) v gets-free(R, chicken)
Move negation in, then drop quantifier:
forall(R): ~pollos(R) v ~cook(R) v gets-free(R, chicken)
14) ~pollos(R) v ~cook(R) v gets-free(R, chicken)
Some cooks like Saul Goodman.
Exist(S): cook(S) ^ likes(S, saul) Now get rid of existential using a skolem constant: cook(todd) ^ likes(todd,saul) Todd is our skolem constant – it can’t be Jesse!
Now split and we have clause form:
15) cook(todd)
16) likes(todd,saul)
Everyone who likes Saul Goodman gets free chicken
This one didn’t say you needed to be in Los Pollos Hermanos, but its fine if you added that too
forall(U): likes(U,saul) -> gets-free(U,chicken)
Get rid of implication, then quantifier:
Forall(U): ~likes(U,saul) v gets-free(U,chicken) 17) ~likes(U,saul) v free(U,chicken)
Now, prove using RR that jesse gets free chicken. We add our negated hypothesis: in this case, that jesse DOESN’T get free chicken.
18) ~gets-free(jesse,chicken)
—
Entire system in clause form, for clarity (you don’t need to repeat it like this for full marks):
1) pollos(jesse)
2) pollos(heisenberg)
3) pollos(gale)
4) pollos(gus)
5) ~welldressed(jesse)
6) ~happy(jesse)
7) likes(heisenberg, poetry)
8) likes(gale, poetry)
9) manager(gus)
10) likes(gus, seafood)
11) ~manager(X) v welldressed(X)
12) happy(Y) v ~likes(Y,Z)
13) ~pollos(Q) v manager(Q) v likes(Q, poetry) v cook(Q) 14) ~pollos(R) v ~cook(R) v gets-free(R, chicken)
15) cook(todd)
16) likes(todd,saul)
17) ~likes(U,saul) v gets-free(U,chicken)
18) ~gets-free(jesse,chicken)
Now, resolutions – substitutions are shown in curly braces, and could be stated in reverse (i.e. T/jesse vs jesse/T as long as you’re consistent – you DO need 2 parents [and ONLY two parents!] and substitutions shown though):
a correct set of resolutions follows – the obvious unsuccessful thing to try is to work with 18 & 17, which can never be fruitful unless you screwed up the existential and made jesse be the cook that magically likes saul without that being stated)
you don’t necessarily have to have started with ~h and worked backward using resolutions derived from it – it’s the most effective way to do it in general though.
19: (18&14, {jesse/R}): ~pollos(jesse) v ~cook(jesse)
20: (19&1): ~cook(jesse)
21: (20&13, {jesse/Q}): ~pollos(jesse) v manager(jesse) v likes(jesse, poetry) 22: (21&1): manager(jesse) v likes(jessy, poetry)
23: (22&13, {jesse/X}): welldressed(jesse) v likes(jesse, poetry)
24: (23&5): likes(jesse, poetry)
25: (24&12, {jesse/Y,poetry/Z}): happy(jesse)
26: (25&6): nil. We have a contradiction that could only come from our negated hypothesis, and thus our original hypothesis, that jesse gets free chicken, is true.
Question 2. 29 Marks (originally incorrectly totaled to 28 on the assignment).
Convert the following sentences into first order logic statements (8 marks – each numbered statement below should be a single FOL statement). This is a more complex system than the previous question; try to be general and think ahead to make the
system practical. You likely want to check out what you want to do with this system (see the rest of the question!) as you do this. Then put these in clause form (8 marks). You must SHOW YOUR WORK if you want any part marks to be considered. Each clause form statement should state the number of the original FOL statement that it came from, and each should also be numbered so the marker can follow your reasoning in the proofs that follow.
1) Spiderman, The Green Goblin, Wolverine, and Mary Jane are persons.
2) The Green Goblin has special powers and he also cheats.
3) The Green Goblin is not a fan of Mary Jane.
4) Spiderman is a mutant, and so is Wolverine.
5) Wolverine is a fan of Captain Picard.
6) All persons with special powers are mutants.
7) All people who do not cheat are good.
8) Some mutants are not X-Men.
9) Mary Jane loves all good persons who are not X-Men.
10) There is no such thing as an X-Man who is not a fan of Captain Picard, and
there is no such thing as an X-Man who cheats.
11) All X-Men are mutants.
12) All mutants who are fans of Captain Picard are X-Men.
13) Spiderman does not cheat and is not a fan of Captain Picard.
Now, using the above system, perform the following proofs using resolution refutation (show your work by stating the numbers of each pair of clauses you are resolving and the necessary substitutions to unify these, numbering each new deduction as we did in class):
i) Prove that Mary Jane loves Spiderman (6 marks).
ii) Prove that Wolverine does not cheat (3 marks).
iii) Consider the statement “there exists an XMan who is a fan of Captain Picard, and Mary Jane loves everyone”. What would the correct clause form null hypothesis be, given your answers to the earlier parts of this question, if you were asked to prove this statement? (4 marks). Note that you are not being asked to prove this (!), just provide the statement in the correct form. As a hint, it will likely help to remember to negate your first-order logic hypothesis first, as we did in the final class example, and then convert to clause form.
First part of Q2 Solution:
This is done with the entire system stated at each phase, but could also be done statement-by-statement like Q1 was.
First order logic statements for each of the above (one fol statement per original!):
1) person(spidey) ^ person(mj) ^ person(w) ^ person(gg)
2) powers(gg,special) ^ cheats(gg) /* could have powers as a 1-place predicate too, but really we’re labeling what kind of powers someone has*/
3) ~fan(gg,mj) /*a 2-place predicate lets us have multiple fans and subjects!*/
4) mutant(spidey) ^ mutant(w)
5) fan(w,picard)
6) forall(X): (person(X) ^ powers(X,special)) -> mutant(X).
7) forall(X) (person(X) ^ ~cheats(X)) -> good(X)
8) exists(X): mutant(X) ^ ~xman(X)
9) forall(X): (person(X) ^ good(X) ^ ~xman(X)) -> loves(mj,X)
10) (~exists(X): (xman(X) ^ ~fan(X,picard))) ^ (~exists(Y): xman(Y) ^ cheats(Y)) /*could also have written 10 with positive foralls, first step of my conversion, but easy to get that wrong!*/
11) forall(X): xman(X) -> mutant(X)
12) forall(X): (mutant(X) ^ fan(X,picard)) -> xman(X)
13) ~cheats(spidey) ^ ~fan(spidey,picard)
Now, clause form: (I’m expecting you to show your work for part marks where you’ve made mistakes)
Statement 1 gives us: 1) person(spidey)
2) person(mj)
3) person(w)
4) person(gg)
Statement 2 gives us 5) powers(gg,special) 6) cheats(gg)
Statement 3 is already in clause form 7) ~fan(gg,mj)
Statement 4 gives us 7) mutant(spidey)
8) mutant(w)
Statement 5 is already in clause form: 9) fan(w,picard)
Statement 6 :
eliminate universals & implies: ~(person(X) ^ powers(X,special)) v mutant(X) now move negation in to get:
10) ~person(X) v ~powers(X,special) v mutant(X)
Statement 7 – follow the same two steps as 6) and get: 11) ~person(C) v cheats(C) v good(C)
Statement 8 – need a skolem constant to get rid of the existential: mutant(hulk) ^ ~xman(hulk)
12) mutant(hulk)
13) ~xman(hulk) /*remember its vital this not be an existing constant!*/ Statement 9 – same two steps as all the implications above, and get
14) ~person(D) v ~good(D) v xman(D) v loves(mj,D)
Statement 10 – get rid of the two ~exists:
(forall(X): ~(xman(X) ^ ~fan(X,picard))) ^ (forall(Y): ~(xman(Y) ^ cheats(Y))) move negations in, get rid of universals:
(~xman(X) v fan(X,picard)) ^ (~xman(Y) v ~cheats(Y))
now separate and standardize variables:
15) ~xman(E) v fan(E,picard) 16) ~xman(F) v ~cheats(F)
Statement 11 – same steps as 9, get: 17) ~xman(G) v mutant(G)
Statement 12 – same steps as 11, get:
18) ~mutant(H) v ~fan(H,picard) v xman(H)
Statement 13 splits to: 19) ~cheats(spidey) 20) ~fan(spidey,picard)
Now, using the above system, perform the following proofs using resolution refutation (show your work by stating the numbers of each pair of clauses you are resolving and the necessary substitutions to unify these, numbering each new deduction as we did in class):
i) Prove that Mary Jane loves Spiderman (6 marks).
This one was worth a couple more marks because there were a couple of places you had to divert to a new chain of resolutions.
~h in clause form is 21) ~loves(mj,spidey). We now attempt to prove a contradiction using resolution refutation. We resolve the following pairs of clauses, producing (substitutions shown):
21 & 14 {spidey/D} gives:
22) ~person(spidey) v ~good(spidey) v xman(spidey)
22 & 1 gives:
23) ~good(spidey) v xman(spidey)
15& 20 {spidey/E} gives: 24) ~xman(spidey)
24& 23 gives:
25) ~good(spidey)
11&25 {spidey/C} gives:
26) ~person(spidey) v cheats(spidey)
26 & 1 gives:
27) cheats(spidey)
and 27& 19 now resolve to nil. contradiction because of ~H, therefore H must be true, and maryjane loves spiderman.
iii) Prove that Wolverine does not cheat (3 marks).
/*simpler than the above, hence less marks*/
If I introduce ~H as
21) cheats(w), I can resolve as follows:
21&16 {w/F} produce 22) ~xman(w)
22&18 {w/H} produce
23) ~mutant(w) v ~fan(w,picard)
23&8 produce
24) ~fan(w,picard)
and 24&9 produce nil. And we know that wolverine doesn’t cheat.
iii) Consider the statement “there exists an XMan who is a fan of Captain Picard, and Mary Jane loves everyone”. What would the correct clause form null hypothesis be, given your answers to the earlier parts of this question, if you were asked to prove this statement? (4 marks). Note that you are not being asked to prove this (!), just provide the statement in the correct form.
/*the key to this is as covered in the notes, negate the hypothesis, then convert to clause form…this is not the same as simply taking the two and-ed halves, and proving your negations separately or together, since it’s not the same statement in clause form */
/*Note that yours may be a little bit different, the point is it has to jive with the way you’ve represented each of these concepts in the proof so far – and my predicates below all jive with my solution above*/
H: (exists(X): xman(X) ^ fan(X,picard)) ^ (forall(Y):loves(mj,Y)) ~H: ~( (exists(X): xman(X) ^ fan(X,picard)) ^ (forall(Y):loves(mj,Y) ) Move negation in:
~(exists(X): xman(X) ^ fan(X,picard)) v ~(forall(Y):loves(mj,Y))
And again:
forall(X): ~( xman(X) ^ fan(X,picard)) v exist(Y):~loves(mj,Y))
And again:
forall(X): ~xman(X) v ~fan(X, picard) v exist(Y):~loves(mj,Y)
Get rid of existential with a skolem constant:
forall(X): ~xman(X) v ~fan(X, picard) v ~loves(mj,flash)
And finally drop the universal:
~xman(X) v ~fan(X, picard) v ~loves(mj,flash)
Question 3: 20 Marks.
Make up your own logical system and a hypothesis to prove on a topic of your choice (try to keep it reasonably family-suitable). Show the statements in English and first order logic, convert them to clause form and solve using resolution refutation as you did for the previous three questions. Your logical system’s statements must use existential and universal quantifiers, and must have at least 8 statements, at least 4 of which should involve implication. Marks will be allocated partly in proportion to the intricacy of your system and the extent of the work you’ve done in representing it, as well as its quality. The system should reason about some set of coherent concepts, be logically correct, semantically correct (i.e. the FOL should capture what you’re saying the English does) and have statements that involve some work (as opposed to just defining individual facts to fill up space). The system must also be entirely your own work, and thus it should also NOT essentially logically duplicate the above examples or the Marcus/Caesar example from class while just changing symbols/subject matter. What you ask to prove should also be possible given your system, and your proof should be done correctly as well.