KR: Exercise 1b

Predicate Calculus: Theorem Proving


In this exercise we will use a theorem prover for Predicate Calculus called Prover9. This prover accepts a list of formulas in First Order Logic (FOL) and decides whether a formula is valid or not by refutation using resolution. We will try to solve several simple exercises by: (1) formulating the exercise in FOL; (2) using prover9 to check whether a conclusion follows from the proposed premises.

Prover9 syntax

Prover9 syntax allows us to write a list of formulas using the following notation

->         implication
&          conjunction
|          disjunction
<->        double implication
-          negation
all x      universal quantifier
exists x   existential quantifier

In principle, the simplest use is by directly writing a set of clauses directly in CNF to check their satisfiability:
  -man(x) | mortal(x).
However, we can also use arbitrary syntax and divide the list of formulas into assumptions and goals, as follows:
  all x (man(x) -> mortal(x)).

Under this second format, Prover9 will negate the goals and add them to the assumptions, passing everything to CNF and using resolution afterwards to decide satisfiability. NOTE: by default Prover9 reads from standard input.

Exercises to solve

  1. All lions are fierce. Some lions do not drink coffee. Therefore, some fierce creatures do not drink coffee.
  2. No professor is ignorant. All ignorant people are vain. So, no professor is vain.
  3. Every poor man has a rich father. Thus, there is a rich man whose grandfather is rich. (NOTE: use a function father(x)).
  4. All hounds howl at night. Anyone who has cats will not have any mice. Light sleepers do not have anything that howls at night. John has either a cat or a hound. Therefore, if John is a light sleeper then he does not have any mice.

Assessment & delivery

The maximum grade for this exercise (1b) is 0,3 points. The deadline for delivery of exercises 1a and 1b is Friday, March 1st, 2013 using the lab work mailbox or buzón de prácticas.

Maintained by Pedro Cabalar. Last update Feb. 14th 2013