Logic for Fun: Demonstrations
The first example is a fairly typical logic puzzle, requiring some philosophically inclined railway workers to be matched up with their jobs. The wrinkle is that half the clues are false, making it a bit more interesting to encode than it might be otherwise.
The second example is again fairly typical of logical puzzles, except that instead of matching up the people with their meetings and so forth, the solver has to find a schedule satisfying all the conditions of the problem. It stops when it finds the smallest solution, so this example also shows how it is possible to express and solve simple optimization problems with this kind of logical system.
The third example is a classic from the field of constraint satisfaction problems. It is not difficult (for the computer) but is chosen to illustrate the convenience of the logical notation as a language for representing such things, and to demonstrate some of the cute effects you can achieve by attending to the way output is presented.
For more examples and a full explanation of the language for encoding them, enter the site and see the "guide" there. If you have not already registered as a user of the site, you will need to do so before you can give yourself a login name (or "User ID") and a password.

