Do the following for each of the following problems:

A. Give clauses to represent it, with negated goal.
B. Create an ordering to compare atoms.
C. Give a refutation proof using Ordered Resolution..
D. Remove one clause of your choice, then saturate the clauses with
Ordered Resolution using subsumption and tautology deletion.  Use the 
model construction technique to create a model.

------------------------------------------------------------------------------

Problem 1:  

Represent the following theorem in propositional logic:

There was a party.  Ann and Bill and Carl and Dave were invited.
Either Ann or Bill (or both) came.  If Ann came then Bill came.  
If Bill came then Ann came.  If Ann and Bill came then Carl came.  
If Bill and Carl came then Dave came.  Therfore, all four of them 
came to the party.

Use a propositional symbol to represent that a given person came
to the party.

------------------------------------------------------------------------------
Problem 2:  

Represent the following theorem in first order logic:

For every number, there is a larger number.  The less-than
predicate is antisymmetric (i.e., if a number is smaller than
another number, then the second number is not smaller than the
first number).  Therefore, there is no largest number.

Use the following predicate:
Less(x,y) - x is less than y


------------------------------------------------------------------------------
Problem 3:  

Represent the following theorem in first order logic:

Every pair of numbers has a product.  x and y divide the product
of x and y.  Therefore, every number divides something.

Use the following predicates:
Prod(x,y,z) - z is the product of x and y
Div(x,y) - x divides y

------------------------------------------------------------------------------
Problem 4:  

Represent the following theorem in propositional logic, like Problem 1:

There was a party.  Ann and Bill and Carl and Debbie were invited.
Either Ann and Bill came or Carl and Debbie came (or both couples came).
Joe claims that if Ann came to the party then Bill didn't come and if
Debbie came then Carl didn't come.  We want to prove that Joe is wrong.

------------------------------------------------------------------------------
Problem 5:  

Represent the following theorem in first order logic:

Everybody in our class has an older brother.
Whenever a person is older than a second person, then the second one is
younger than the first.
Whenever a person is a brother of a second person, then the second one is
a sibling of the first.
Whenver a person is a sibling of a second person, and the first one is male,
then the first person is a brother of the second.
There is a male in our class.
Therefore there is a person who has a younger brother. (Note: I did not
say whether this person is in our class)

Use the following predicates:
C(x) - x is in our class
O(x,y) - x is older than y
Y(x,y) - x is younger than y
B(x,y) - x is a brother of y
S(x,y) - x is a sibling of y
M(x) - x is male

------------------------------------------------------------------------------