Your problem is to use first-order 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: impostor.p9
Marks: There are two marks for each sentence, making a total of 28 marks.
| A1 | Blue,Red,Yellow, Purple and a Janitor are crewmembers on a ship and are the only crewmembers. |
| A2 | There are two crewmembers who are impostors. |
| A3 | There are no more than two impostors. |
| A4 | If somebody accuses someone then the accused is an impostor or the accuser is the impostor. |
| A5 | If somebody is known to be an impostor, then they are an impostor. |
| A6 | Impostors know they are impostors. |
| A7 | If someone is murdered then they are not an impostor. |
| A8 | Purple knows one of the impostors. |
| A9 | Purple doesn't know that the Janitor or Blue are an impostor. |
| A10 | Purple was found murdered. |
| A11 | Neither Red or Blue are the Janitor. |
| A12 | Blue accused Yellow. |
| A13 | Nobody knows that Yellow is an impostor. |
| Goal | Yellow, Purple and the Janitor are not impostors and Blue and Red are impostors. |
Predicates: Crewmember, Impostor, Murdered
Relations: Accused, KnowsImpostor