EpiPEn is a Python library for expressing and solving epistemic puzzles – puzzles that require reasoning about knowledge and ignorance. For example, take this puzzle:

Anne and Bill are told the following: “I have two natural numbers. They are consecutive numbers. I am going to whisper one of these numbers to Anne and the other number to Bill.” This happens. Anne and Bill then have the following conversation:Anne: “I don’t know your number.”How is this possible? What are their numbers?

Bill: “I don’t know your number.”

Anne: “I know your number.”

Bill: “I know your number.”

With EpiPEn, you can express and solve this puzzle like this:

from epipen import * from z3 import * start_story() Anne, Bill = Characters('Anne Bill') A, B = Ints('A B') announce(storyteller, And(A >= 0, B >= 0, Or(A == B + 1, B == A + 1))) learn_constant(Anne, A) learn_constant(Bill, B) announce(Anne, Not(know(value_of=B))) announce(Bill, Not(know(value_of=A))) announce(Anne, know(value_of=B)) announce(Bill, know(value_of=A)) print_possible_worlds()

Pulling this off requires a novel encoding of epistemic logic in first-order logic and some embedded-DSL shenanigans. Pretty neat!

Read more about Relat in:

EpiPEn was my final project for CSE 507. It was a collaboration with Jack Zhang.