Angry Dragons

A logic problem by Adam Richard-Bollans

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: dragons.p9

Marks: There are two marks for each sentence, making a total of 10 marks.

Problem Statement

A1	If the dragon destroys the village, the villagers will be homeless unless they take the King's Castle.
A2	If the King is mean then the villagers will take the castle.
A3	If the King is not mean then the dragon won't destroy the village.
A4	The dragon destroys the village.
Goal	The villagers are not homeless.

Non-Logical Vocabulary

Propositional Constants: DragonDestroysVillage, VillagersTakeCastle, VillagersHomeless, KingMean

Notes:

In A1 there may be multiple ways to interpret `unless'. If the villagers take the castle will they be homeless? You may have arrived at a different solution and this problem highlights some of the challenges of translating natural language to formal logic.