Skip to content

Instantly share code, notes, and snippets.

@lgessler

lgessler/floors.txt

Created October 9, 2019 23:27
Show Gist options
  • Save lgessler/73d442ef4da8435109e9fa661caddeb2 to your computer and use it in GitHub Desktop.
Save lgessler/73d442ef4da8435109e9fa661caddeb2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
floors.txt
// This is an adaptation of a logic puzzle presented in SICP
// (https://web.mit.edu/alexmv/6.037/sicp.pdf#page=596) and respectively
// sourced from Dinesman 1968:
//
// > Baker, Cooper, Fletcher, Miller, and Smith live on different floors of an
// > apartment house that contains only five floors. Baker does not live on the
// > top floor. Cooper does not live on the bottom floor. Fletcher does not live
// > on either the top or the bottom floor. Miller lives on a higher floor than
// > does Cooper. Smith does not live on a floor adjacent to Fletcher’s. Fletcher
// > does not live on a floor adjacent to Cooper’s. Where does everyone live?
// We need these constants:
// - Baker, Cooper, Fletcher, Miller, Smith
(person Baker)
(person Cooper)
(person Fletcher)
(person Miller)
(person Smith)
// - first, second, third, fourth, fifth
(floor First)
(floor Second)
(floor Third)
(floor Fourth)
(floor Fifth)
// > Baker, Cooper, Fletcher, Miller, and Smith live on different floors of an
// > apartment house that contains only five floors.
// I.e., there are no two people who inhabit the same floor
// We can't use this formula because we can't enforce that x != y in any way...
// (forall x (forall y (forall z (cond (and (person x) (person y)) (not (and (inhabits x z) (inhabits y z)))))))
// so we need to expand it:
(forall z (cond (floor z) (or (and (inhabits Baker z) (and (not (inhabits Cooper z)) (and (not (inhabits Fletcher z)) (and (not (inhabits Miller z)) (not (inhabits Smith z)))))) (or (and (inhabits Cooper z) (and (not (inhabits Baker z)) (and (not (inhabits Fletcher z)) (and (not (inhabits Miller z)) (not (inhabits Smith z)))))) (or (and (inhabits Fletcher z) (and (not (inhabits Cooper z)) (and (not (inhabits Baker z)) (and (not (inhabits Miller z)) (not (inhabits Smith z)))))) (or (and (inhabits Miller z) (and (not (inhabits Cooper z)) (and (not (inhabits Fletcher z)) (and (not (inhabits Baker z)) (not (inhabits Smith z)))))) (and (inhabits Smith z) (and (not (inhabits Cooper z)) (and (not (inhabits Fletcher z)) (and (not (inhabits Miller z)) (not (inhabits Baker z))))))))))))
// more legibly:
// (forall z
// (cond
// (floor z)
// (or
// (and (inhabits Baker z)
// (and (not (inhabits Cooper z))
// (and (not (inhabits Fletcher z))
// (and (not (inhabits Miller z))
// (not (inhabits Smith z))))))
// (or
// (and (inhabits Cooper z)
// (and (not (inhabits Baker z))
// (and (not (inhabits Fletcher z))
// (and (not (inhabits Miller z))
// (not (inhabits Smith z))))))
// (or
// (and (inhabits Fletcher z)
// (and (not (inhabits Cooper z))
// (and (not (inhabits Baker z))
// (and (not (inhabits Miller z))
// (not (inhabits Smith z))))))
// (or
// (and (inhabits Miller z)
// (and (not (inhabits Cooper z))
// (and (not (inhabits Fletcher z))
// (and (not (inhabits Baker z))
// (not (inhabits Smith z))))))
// (and
// (inhabits Smith z)
// (and (not (inhabits Cooper z))
// (and (not (inhabits Fletcher z))
// (and (not (inhabits Miller z))
// (not (inhabits Baker z))))))))))))
// > Baker does not live on the top floor.
(not (inhabits Baker Fifth))
// > Cooper does not live on the bottom floor.
(not (inhabits Cooper First))
// > Fletcher does not live on either the top or the bottom floor.
(not (or (inhabits Fletcher First) (inhabits Fletcher Fifth)))
// > Miller lives in a higher floor than does Cooper.
(or (and (inhabits Cooper First) (inhabits Miller Second)) (or (and (inhabits Cooper First) (inhabits Miller Third)) (or (and (inhabits Cooper First) (inhabits Miller Fourth)) (or (and (inhabits Cooper First) (inhabits Miller Fifth)) (or (and (inhabits Cooper Second) (inhabits Miller Third)) (or (and (inhabits Cooper Second) (inhabits Miller Fourth)) (or (and (inhabits Cooper Second) (inhabits Miller Fifth)) (or (and (inhabits Cooper Third) (inhabits Miller Fourth)) (or (and (inhabits Cooper Third) (inhabits Miller Fifth)) (and (inhabits Cooper Fourth) (inhabits Miller Fifth)))))))))))
// more legibly:
// (or
// (and
// (inhabits Cooper First)
// (inhabits Miller Second))
// (or
// (and
// (inhabits Cooper First)
// (inhabits Miller Third))
// (or
// (and
// (inhabits Cooper First)
// (inhabits Miller Fourth))
// (or
// (and
// (inhabits Cooper First)
// (inhabits Miller Fifth))
// (or
// (and
// (inhabits Cooper Second)
// (inhabits Miller Third))
// (or
// (and
// (inhabits Cooper Second)
// (inhabits Miller Fourth))
// (or
// (and
// (inhabits Cooper Second)
// (inhabits Miller Fifth))
// (or
// (and
// (inhabits Cooper Third)
// (inhabits Miller Fourth))
// (or
// (and
// (inhabits Cooper Third)
// (inhabits Miller Fifth))
// (and
// (inhabits Cooper Fourth)
// (inhabits Miller Fifth)))))))))))
// > Smith does not live on a floor adjacent to Fletcher's
(not (or (and (inhabits Smith First) (inhabits Fletcher Second)) (or (and (inhabits Smith Second) (inhabits Fletcher First)) (or (and (inhabits Smith Second) (inhabits Fletcher Third)) (or (and (inhabits Smith Third) (inhabits Fletcher Second)) (or (and (inhabits Smith Third) (inhabits Fletcher Fourth)) (or (and (inhabits Smith Fourth) (inhabits Fletcher Third)) (or (and (inhabits Smith Fourth) (inhabits Fletcher Fifth)) (and (inhabits Smith Fifth) (inhabits Fletcher Fourth))))))))))
// more legibly:
// (not
// (or
// (and
// (inhabits Smith First)
// (inhabits Fletcher Second))
// (or
// (and
// (inhabits Smith Second)
// (inhabits Fletcher First))
// (or
// (and
// (inhabits Smith Second)
// (inhabits Fletcher Third))
// (or
// (and
// (inhabits Smith Third)
// (inhabits Fletcher Second))
// (or
// (and
// (inhabits Smith Third)
// (inhabits Fletcher Fourth))
// (or
// (and
// (inhabits Smith Fourth)
// (inhabits Fletcher Third))
// (or
// (and
// (inhabits Smith Fourth)
// (inhabits Fletcher Fifth))
// (and
// (inhabits Smith Fifth)
// (inhabits Fletcher Fourth))))))))))
// > Fletcher does not live on a floor adjacent to Cooper's
(not (or (and (inhabits Cooper First) (inhabits Fletcher Second)) (or (and (inhabits Cooper Second) (inhabits Fletcher First)) (or (and (inhabits Cooper Second) (inhabits Fletcher Third)) (or (and (inhabits Cooper Third) (inhabits Fletcher Second)) (or (and (inhabits Cooper Third) (inhabits Fletcher Fourth)) (or (and (inhabits Cooper Fourth) (inhabits Fletcher Third)) (or (and (inhabits Cooper Fourth) (inhabits Fletcher Fifth)) (and (inhabits Cooper Fifth) (inhabits Fletcher Fourth))))))))))
// More legibly:
// (not
// (or
// (and
// (inhabits Cooper First)
// (inhabits Fletcher Second))
// (or
// (and
// (inhabits Cooper Second)
// (inhabits Fletcher First))
// (or
// (and
// (inhabits Cooper Second)
// (inhabits Fletcher Third))
// (or
// (and
// (inhabits Cooper Third)
// (inhabits Fletcher Second))
// (or
// (and
// (inhabits Cooper Third)
// (inhabits Fletcher Fourth))
// (or
// (and
// (inhabits Cooper Fourth)
// (inhabits Fletcher Third))
// (or
// (and
// (inhabits Cooper Fourth)
// (inhabits Fletcher Fifth))
// (and
// (inhabits Cooper Fifth)
// (inhabits Fletcher Fourth))))))))))
// > Where does everyone live?
(and (inhabits Baker Third) (and (inhabits Cooper Second) (and (inhabits Fletcher Fourth) (and (inhabits Miller Fifth) (inhabits Smith First)))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment