## 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