Your problem is to use propositional logic to represent the following example of reasoning, and use the Prover9 theorem prover to prove that the reasoning is valid.
Use the following template file to create your Prover9 encoding of the problem: tarquin.p9
Marks: There are two marks for each sentence, making a total of 12 marks.
| A1 | If Tarquin learns philosophy then he acquires wisdom and if he learns science he will advance human knowledge. |
| A2 | If he acquires wisdom, Tarquin will not die in misery. |
| A3 | If he advances human knowledge, his aspirations will be satisfied. |
| A4 | If Tarquin's aspirations are not satisfied he will die in misery. |
| A5 | Alas, Tarquin's aspirations will never be satisfied |
| Goal | Thus, he learns neither philosophy nor science |