KR: Exercise 1b

Predicate Calculus: Theorem Proving

Introduction

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; (3) if the conclusion does not follow from the premises, then try including any commonsense additional axiom that could be missing.

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:
formulas(sos).
  -man(x) | mortal(x).
  man(socrates).
  -mortal(socrates).
end_of_list.
However, we can also use arbitrary syntax and divide the list of formulas into assumptions and goals, as follows:
formulas(assumptions).
  all x (man(x) -> mortal(x)).
  man(socrates).
end_of_list.

formulas(goals).
  mortal(socrates).
end_of_list.
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. Every poor man has a rich father. Thus, there is a rich man whose grandfather is rich. (NOTE: use a function father(x)).
  2. An equivalence relation eq(x,y) satisfies the axioms of reflexivity, symmetry and transitivity. Prove that for two elements x, y that are not equivalent, there is no third element that is equivalent to both x and y.
  3. Workers in a company dislike all rival companies. There is a worker whose boss likes everything. Then try to conclude that there is some company without rival companies.
  4. An herbivore never eats animals. The shark eats fishes and, obviously, fishes are animals. Then, the shark cannot be an herbivore.

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 7th, 2014 using the lab work mailbox or buzón de prácticas.


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