Question Mark: $20$

Note that all of these proofs require resolution refutation: no marks are available for any other form of reasoning.

Make up your own logical system and a hypothesis to prove on a topic of your choice $($and try to keep it reasonably

family$-$suitable, ok$?).$ Show the statements in English and first order logic, convert them to clause form and solve using

resolution refutation $($See the example question below, but make your own which has no relation to the example$).$ 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 in proportion to the intricacy of your system and the extent

of the work you've done in representing it$.$ The system should reason about some set of coherent concepts as the

questions above do$,$ be logically correct, 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.

Example $($just to help you understand the format; also this example is just a question part; you should not only have a

new question but also its solution or proof$)$:

"Convert the following sentences into first order logic statements $($each numbered statement below should be a single

FOL statement$).$ Then put these in clause form. 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. Each new resolution

should show the two parents clauses used to derive the resolution. You must also state the necessary substitutions for

unification where unification is performed.

Spiderman, The Green Goblin, Wolverine, and Mary Jane are persons.

The Green Goblin has special powers and he also cheats.

The Green Goblin is not a fan of Mary Jane.

Spiderman is a mutant, and so is Wolverine.

Wolverine is a fan of Captain Picard.

All persons with special powers are mutants.

All people who do not cheat are good.

Some mutants are not X$-$Men.

Mary Jane loves all good persons who are not $x-$Men.

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.

All X$-$Men are mutants.

All mutants who are fans of Captain Picard are X$-$Men.

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.

ii$)$ Prove that Wolverine does not cheat."