Description
For this assignment, you will use Prover9 – an automated theorem prover for first-order logic.
Consider the sentences given below:
1. Anyone who eats a pizza is a happy character
2. Every foodie eats [something that is] either a pizza or a salad
3. Anyone who eats a salad is healthy
4. Every healthy person goes to the gym
5. Any nice girl does not date anyone who is a happy character
6. Ann is a nice girl, and Peter is a foodie
7. (Conclusion) If Peter does not go to gym, then Ann does not date Peter.
Represent these sentences in first order logic, using only these predicates:
Eats(x,y), Pizza(x), Salad(x), Happy(x), Healthy(x), Foodie(x), Gyms(x), Nice(x), Dated(x,y).
Using Prover9, show that the conclusion is true by using resolution refutation.
Submit a report with the following details:
• Assumptions and goal
• The input and output of prover9. (Paste as plain text in the report)
• Conclusion
Some useful links:
1. Installation
For linux users, install python-wxtools also.
2. Help Manual
3. Simple tutorial
1
