← Josh Horowitz


Epistemic Programming Environment

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.”
Bill: “I don’t know your number.”
Anne: “I know your number.”
Bill: “I know your number.”
How is this possible? What are their numbers?

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

from epipen import *
from z3 import *

Anne, Bill = Characters('Anne Bill')
A, B = Ints('A B')

    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))


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 paper thumbnail
The paper
EpiPEn slideshow thumbnail
The slides

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