| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
Description
From Raymond Smullyan: On a fictional island, all inhabitants are either knights, who always tell the truth, or knaves, who always lie. John and Bill are residents of the island of knights and knaves. John and Bill make several utterances. Determine which one is a knave or a knight, depending on their answers.
Synopsis
- data Inhabitant
- cv2Inhabitant :: String -> [CV] -> Inhabitant
- _undefiner_Inhabitant :: a
- type SInhabitant = SBV Inhabitant
- data Identity
- cv2Identity :: String -> [CV] -> Identity
- _undefiner_Identity :: a
- type SIdentity = SBV Identity
- sKnave :: SBV Identity
- sKnight :: SBV Identity
- isKnave :: SBV Identity -> SBool
- isKnight :: SBV Identity -> SBool
- sCaseIdentity :: Mergeable result => SBV Identity -> result -> result -> result
- data Statement
- cv2Statement :: String -> [CV] -> Statement
- _undefiner_Statement :: a
- type SStatement = SBV Statement
- sTruth :: SBV Statement
- sFalsity :: SBV Statement
- isTruth :: SBV Statement -> SBool
- isFalsity :: SBV Statement -> SBool
- sCaseStatement :: Mergeable result => SBV Statement -> result -> result -> result
- john :: SInhabitant
- bill :: SInhabitant
- is :: SInhabitant -> SIdentity -> SStatement
- says :: SInhabitant -> SStatement -> SBool
- holds :: SStatement -> SBool
- and :: SStatement -> SStatement -> SStatement
- not :: SStatement -> SStatement
- iff :: SStatement -> SStatement -> SStatement
- puzzle :: IO ()
Documentation
data Inhabitant Source #
Inhabitants of the island, as an uninterpreted sort
Instances
cv2Inhabitant :: String -> [CV] -> Inhabitant Source #
Conversion from SMT values to Inhabitant values.
_undefiner_Inhabitant :: a Source #
Autogenerated definition to avoid unused-variable warnings from GHC.
type SInhabitant = SBV Inhabitant Source #
Symbolic version of the type Inhabitant.
Each inhabitant is either a knave or a knight
Instances
_undefiner_Identity :: a Source #
Autogenerated definition to avoid unused-variable warnings from GHC.
sCaseIdentity :: Mergeable result => SBV Identity -> result -> result -> result Source #
Case analyzer for the type Identity.
Statements are utterances which are either true or false
Instances
_undefiner_Statement :: a Source #
Autogenerated definition to avoid unused-variable warnings from GHC.
sCaseStatement :: Mergeable result => SBV Statement -> result -> result -> result Source #
Case analyzer for the type Statement.
john :: SInhabitant Source #
John is an inhabitant of the island.
bill :: SInhabitant Source #
Bill is an inhabitant of the island.
is :: SInhabitant -> SIdentity -> SStatement Source #
The connective is makes a statement about an inhabitant regarding his/her identity.
says :: SInhabitant -> SStatement -> SBool Source #
The connective says makes a predicate from what an inhabitant states
and :: SStatement -> SStatement -> SStatement Source #
The connective and creates the conjunction of two statements
not :: SStatement -> SStatement Source #
The connective not negates a statement
iff :: SStatement -> SStatement -> SStatement Source #
The connective iff creates a statement that equates the truth values of its argument statements
Encode Smullyan's puzzle. We have:
>>>puzzleQuestion 1. John says, We are both knaves Then, John is: Knave And, Bill is: Knight Question 2. John says If (and only if) Bill is a knave, then I am a knave. Bill says We are of different kinds. Then, John is: Knave And, Bill is: Knight