You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
76 lines
2.1 KiB
76 lines
2.1 KiB
from logic import *
|
|
|
|
AKnight = Symbol("A is a Knight")
|
|
AKnave = Symbol("A is a Knave")
|
|
|
|
BKnight = Symbol("B is a Knight")
|
|
BKnave = Symbol("B is a Knave")
|
|
|
|
CKnight = Symbol("C is a Knight")
|
|
CKnave = Symbol("C is a Knave")
|
|
|
|
# Puzzle 0
|
|
# A says "I am both a knight and a knave."
|
|
knowledge0 = And(
|
|
Not(And(AKnave, AKnight)),
|
|
Or(AKnave, AKnight),
|
|
Implication(AKnight, And(AKnave, AKnight))
|
|
)
|
|
|
|
# Puzzle 1
|
|
# A says "We are both knaves."
|
|
# B says nothing.
|
|
knowledge1 = And(
|
|
Not(And(AKnave, AKnight)), Or(AKnave, AKnight),
|
|
Not(And(BKnave, BKnight)), Or(BKnave, BKnight),
|
|
Implication(AKnight, And(AKnave, BKnave)),
|
|
Implication(AKnave, Not(And(AKnave, BKnave)))
|
|
)
|
|
|
|
# Puzzle 2
|
|
# A says "We are the same kind."
|
|
# B says "We are of different kinds."
|
|
knowledge2 = And(
|
|
Not(And(AKnave, AKnight)), Or(AKnave, AKnight),
|
|
Not(And(BKnave, BKnight)), Or(BKnave, BKnight),
|
|
Implication(AKnight, And(AKnight, BKnight)),
|
|
Implication(BKnave, And(AKnight, BKnight)),
|
|
Implication(BKnight, And(Not(And(BKnight, AKnight)), Not(And(BKnave, AKnave))))
|
|
)
|
|
|
|
# Puzzle 3
|
|
# A says either "I am a knight." or "I am a knave.", but you don't know which.
|
|
# B says "A said 'I am a knave'."
|
|
# B says "C is a knave."
|
|
# C says "A is a knight."
|
|
knowledge3 = And(
|
|
Not(And(AKnave, AKnight)), Or(AKnave, AKnight),
|
|
Not(And(BKnave, BKnight)), Or(BKnave, BKnight),
|
|
Not(And(CKnave, CKnight)), Or(CKnave, CKnight),
|
|
Implication(AKnave, AKnight),
|
|
Biconditional(AKnave, BKnight),
|
|
Biconditional(BKnave, CKnight),
|
|
Biconditional(AKnight, CKnight)
|
|
)
|
|
|
|
|
|
def main():
|
|
symbols = [AKnight, AKnave, BKnight, BKnave, CKnight, CKnave]
|
|
puzzles = [
|
|
("Puzzle 0", knowledge0),
|
|
("Puzzle 1", knowledge1),
|
|
("Puzzle 2", knowledge2),
|
|
("Puzzle 3", knowledge3)
|
|
]
|
|
for puzzle, knowledge in puzzles:
|
|
print(puzzle)
|
|
if len(knowledge.conjuncts) == 0:
|
|
print(" Not yet implemented.")
|
|
else:
|
|
for symbol in symbols:
|
|
if model_check(knowledge, symbol):
|
|
print(f" {symbol}")
|
|
|
|
|
|
if __name__ == "__main__":
|
|
main()
|