sbv-8.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Description

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

Puzzle:

You are standing in front of three rooms and must choose one. In one room is a Lady (whom you could and wish to marry), in the other two rooms are tigers (that if you choose either of these rooms, the tiger invites you to breakfast – the problem is that you are the main course). Your job is to choose the room with the Lady. The signs on the doors are:

• A Tiger is in this room
• A Lady is in this room
• A Tiger is in room two

At most only 1 statement is true. Where’s the Lady?

Synopsis

# Documentation

Prints the only solution:

>>> ladyAndTigers
Solution #1:
sign1  = False :: Bool
sign2  = False :: Bool
sign3  =  True :: Bool
tiger1 = False :: Bool
tiger2 =  True :: Bool
tiger3 =  True :: Bool
This is the only solution.


That is, the lady is in room 1, and only the third room's sign is true.