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.
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
- All lions are fierce. Some lions do not drink coffee.
Therefore, some fierce creatures do not drink coffee.
- No professor is ignorant. All ignorant people are
vain. So, no professor is vain.
- Every poor man has a rich father. Thus, there is a
rich man whose grandfather is rich. (NOTE: use a
function father(x)).
- 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.
|