Question 1. Prove using PROPOSITIONAL logic and Prover9 that the map that includes only Chile, Peru, Argentina and Bolivia (cf. Fig. 1) cannot be painted with 2 colors if adjacent countries must have different colors. To simplify, assume that the colors are blue and green.
More precisely:
(a) Write in propositional logic, outside Prover9, the knowledge basis.
(b) Describe the methodology you will use (all this before going into Prover9).
(c) Do the proof with Prover9, including the text file for/by Prover9 as an appendix (better use the verbatim environment in Latex).
It has to contain all the formulas, the run, and the final clean proof.
Figure 1: Map of South America
(d) Discuss to what extent your methodology is general and declarative (as opposed to a hack for this very particular problem). In particular, would your program be essentially different it the question were about coloring with 3 colors?
Question 2. There are two sealed boxes, of gold and silver. It is known that only one of them contains the diamond. Each of the boxes has a label on top, saying:
• Label on Gold Box: "The diamond is not here".
• Label on Silver Box: "Exactly one of the labels is true".
- It is also known that at most one of the labels is true. Determine using PROPOSITIONAL logic and Prover9 where the diamond is. More specifically,
(a) Write a propositional knowledge basis describing the above situation. Explain.
(b) Describe how to use Prover9 to deduce in which box is the diamond. Include the file and run as in problem 1.
(c) Explain what Prover9 did.
Question 3. An equivalence relation (ER) on a set can be seen as a structure (A, R), where
A is a non-empty set, and R ⊆ A × A is a binary relation with the following properties:
1. For every a ∈ A : (a, a) ∈ R (reflexivity)
2. For every a, b ∈ A : (a, b) ∈ R ⇒ (b, a) ∈ R (symmetry)
3. For every a, b, c ∈ A : (a, b) ∈ R and (b, c) ∈ R ⇒ (a, c) ∈ R (transitivity)
(a) Show a concrete finite ER on a finite set, including the proof that it is an ER.
(b) Prove, as usual, from 1. - 3. the following theorem of the theory of ERs: (no Prover9 here)
"For every a, b, c ∈ A : (a, c) ∈ R and (b, c) ∈ R ⇒ (a, b) ∈ R"
(c) Show by means of a finite example (structure) that: 1. & 2. 
3.
That is, a counterexample that proves the independence of 3. from 1. and 2.
(d) Show with a finite example (structure) that: 1. & 2. ¬3.
That is, a counterexample that proves the consistency of 3. with 1. and 2.
(¬3. is: "There are a, b, c ∈ A with: (a, b) ∈ R, (b, c) ∈ R, and (a, c) ∉ R")