// First, let's give some type-variables some values: Nationality = Englishman | Swede | Dane | Norwegian | German Colour = Red | Green | Yellow | Blue | White Cigarette = PallMall | Dunhill | BlueMaster | Blend | Prince Domestic = Dog | Bird | Cat | Zebra | Horse Beverage = Tea | Coffee | Milk | Beer | Water HouseRow = First | Second | Third | Fourth | Fifth { We use injections to make the array-elements unique. Example: 'Pet' is an array of unique elements of type 'Domestic', indexed by 'Nationality'. In the predicate 'Zebra', we use this injection 'Pet' to define the array-variable 'pet' as a parameter of the 'Zebra'-predicate. The symbol used is the '->>'. 'Nationality->>Domestic' can be read as 'Domestic(Nationality)' in "plain array-speak"; the difference being that the elements are by definition unique (cf. 'injective function'). So, in FormulaOne we use a formula like: 'pet(Swede) = Dog', which simply means that the 'Swede' (type 'Nationality') has a 'pet' (type 'Pet', of type 'Domestic', indexed by 'Nationality'), which appears to be a 'Dog' (type 'Domestic'). Or, one could say that the 'Swede' has been mapped to the 'Dog' (Oh, well...). } Pet = Nationality->>Domestic Drink = Nationality->>Beverage HouseColour = Nationality->>Colour Smoke = Nationality->>Cigarette HouseOrder = HouseRow->>Nationality pred Zebra(house_olour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff // For convenience sake, some temporary place_holder variables are used. // An underscore distinguishes them: house_colour(green_house) = Green & house_colour(white_house) = White & house_colour(yellow_house) = Yellow & smoke(pallmall_smoker) = PallMall & smoke(blend_smoker) = Blend & smoke(dunhill_smoker) = Dunhill & smoke(bluemaster_smoker) = BlueMaster & pet(cat_keeper) = Cat & pet(neighbour_dunhill_smoker) = Horse & { 2. The English man lives in the red house: } house_colour(Englishman) = Red & { 3. The Swede has a dog: } pet(Swede) = Dog & { 4. The Dane drinks tea: } drink(Dane) = Tea & { 'smoke' and 'drink' are both nouns, like the other variables. One could read the formulas like: 'the colour of the Englishman's house is Red' -> 'the Swede's pet is a dog' -> 'the Dane's drink is tea'. } { 5. The green house is immediately to the left of the white house. The local predicate 'LeftOf' (see below) determines the house order: } LeftOf(green_house, white_house, house_order) & { 6. They drink coffee in the green house: } drink(green_house) = Coffee & { 7. The man who smokes Pall Mall has birds: } pet(pallmall_smoker) = Bird & { 8. In the yellow house they smoke Dunhill: } smoke(yellow_house) = Dunhill & { 9. In the middle house (third in the row) they drink milk: } drink(house_order(Third)) = Milk & {10. The Norwegian lives in the first house: } house_order(First) = Norwegian & {11. The man who smokes Blend lives in the house next to the house with cats. Another local predicate 'Neighbour' makes them neighbours: } Neighbour(blend_smoker, cat_keeper, house_order) & {12. In a house next to the house where they have a horse, they smoke Dunhill: } Neighbour(dunhill_smoker, neighbour_dunhill_smoker, house_order) & {13. The man who smokes Blue Master drinks beer: } drink(bluemaster_smoker) = Beer & {14. The German smokes Prince: } smoke(German) = Prince & {15. The Norwegian lives next to the blue house Cf. 10. "The Norwegian lives in the first house", so the blue house is the second house: } house_colour(house_order(Second)) = Blue & {16. They drink water in a house next to the house where they smoke Blend: } drink(neighbour_blend_smoker) = Water & Neighbour(blend_smoker, neighbour_blend_smoker, house_order) { A simplified solution would number the houses 1, 2, 3, 4, 5 which makes it easier to order the houses. 'right in the center' would become 3; 'in the first house', 1 But we stick to the original puzzle and use some local predicates. } local pred Neighbour(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder)iff neighbour1 <> neighbour2 & house_order(house1) = neighbour1 & house_order(house2) = neighbour2 & ( house1 = house2 + 1 | house1 = house2 - 1 ) local pred LeftOf(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder) iff neighbour1 <> neighbour2 & house_order(house1) = neighbour1 & house_order(house2) = neighbour2 & house1 = house2 - 1 { The 'all'-query in FormulaOne: all Zebra(house_colour, pet, smokes, drinks, house_order) gives, of course, only one solution, so it can be replaced by: one Zebra(house_colour, pet, smokes, drinks, house_order) } // The compacted version: Nationality = Englishman | Swede | Dane | Norwegian | German Colour = Red | Green | Yellow | Blue | White Cigarette = PallMall | Dunhill | BlueMaster | Blend | Prince Domestic = Dog | Bird | Cat | Zebra | Horse Beverage = Tea | Coffee | Milk | Beer | Water HouseRow = First | Second | Third | Fourth | Fifth Pet = Nationality->>Domestic Drink = Nationality->>Beverage HouseColour = Nationality->>Colour Smoke = Nationality->>Cigarette HouseOrder = HouseRow->>Nationality pred Zebra(house_colour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff house-colour(green_house) = Green & house-colour(white_house) = White & house-colour(yellow_house) = Yellow & smoke(pallmall_smoker) = PallMall & smoke(blend_smoker) = Blend & smoke(dunhill_smoker) = Dunhill & smoke(bluemaster_smoker) = BlueMaster & pet(cat_keeper) = Cat & pet(neighbour_dunhill_smoker) = Horse & house_colour(Englishman) = Red & pet(Swede) = Dog & drink(Dane) = Tea & LeftOf(green_house, white_house, house_order) & drink(green_house) = Coffee & pet(pallmall_smoker) = Bird & smoke(yellow_house) = Dunhill & drink(house_order(Third)) = Milk & house_order(First) = Norwegian & Neighbour(blend_smoker, cat_keeper, house_order) & Neighbour(dunhill_smoker, neighbour_dunhill_smoker, house_order) & drink(bluemaster_smoker) = Beer & smoke(German) = Prince & house_colour(house_order(Second)) = Blue & drink(neighbour_blend_smoker) = Water & Neighbour(blend_smoker, neighbour_blend_smoker, house_order) local pred Neighbour(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder)iff neighbour1 <> neighbour2 & house_order(house1) = neighbour1 & house_order(house2) = neighbour2 & ( house1 = house2 + 1 | house1 = house2 - 1 ) local pred LeftOf(neighbour1::Nationality, neighbour2::Nationality, house_::HouseOrder) iff neighbour1 <> neighbour2 & house_order(house1) = neighbour1 & house_order(house2) = neighbour2 & house1 = house2 - 1