Languages

You are here

Homework assignment

Predicate Calculus exercises

With each exercise below, complete the following steps:

  1. Formalize the premises and the coclusion using a suitable Predicate Calculus representation.
  2. Try to obtain a formal proof for the conclusion using any inference method of your choice: axiomatic, tableaux, natural deduction, resolution, etc. If the conclusion does not follow from the premises, try to build a counterexample.
  3. Use the automated theorem prover prover9 to check the result you obtained by hand.

Exercise 1 (Lewis Carroll)

  • All lions are fierce;
  • Some lions do not drink coffee;
  • Therefore, some fierce creatures do not drink coffee.

Exercise 2 (Lewis Carroll)

  • No professors are ignorant;
  • All ignorant people are vain;
  • Therefore, no professors are vain.

Exercise 3: The rich grandfather riddle

  • Every poor man has a rich father
  • Thus, there is a rich man whose grandfather is rich.

NOTES: we assume rich and poor are opposite concepts; use function "father(x)".

Exercise 4

  • All hounds howl at night.
  • Anyone who has any cats will not have any mice.
  • Light sleepers do not have anything which howls at night.
  • John has either a cat or a hound.
  • Therefore, if John is a light sleeper, then John does not have any mice.

NOTE: prove the conclusion using resolution.