Have you ever tried to solve the famous Einstein's logic puzzle? It is claimed that only 2% of the world's population can solve it!
The ontology has been created using Protege 4.0. It contains the original formulation of the puzzle taken from http://en.wikipedia.org/wiki/Zebra_puzzle. For convenience, all key axioms in the ontology are provided with annotation, a corresponding condition of the puzzle.
Just classify this ontology in Protege and get a solution by clicking on individuals!
The formalization of Einstein's puzzle in a description logic is just one way to solve it automatically. It is a compact (in the number of signature symbols used) and convenient (close to natural language) presentation of the puzzle. Note however that these kinds of puzzles can be easily formalized in pure propositional logic and solved by SAT solvers. Typically, a riddle can be viewed as a k×n matrix and encoded as a SAT problem with k×n2 propositional variables. For 1 ≤ i ≤ k, 1 ≤ j ≤ n, and 1 ≤ m ≤ n, we consider a variable Pijm to be true iff the (i,j)-entry in the matrix has value m.
Finally, here is the formulation of the riddle from http://en.wikipedia.org/wiki/Zebra_puzzle:
Now, who drinks water? Who owns the zebra?
In the interest of clarity, it must be added that each of the five houses is painted a different color, has a single inhabitant, and the inhabitants are of different national extractions, own different pets, drink different beverages and smoke different brands of American cigarettes. In statement 6, right refers to the reader's right.