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
- Every poor man has a rich father. Thus, there is a
rich man whose grandfather is rich. (NOTE: use a
function father(x)).
- 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.
- 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.
- 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.
|