Solutions to Logic Exercises

-------------------------------------------------------------------------------

Properties of Binary Relations
(solution by Martin Ouimet)

1. The non-empty property can be removed.
   Relation satisfying the remaining properties:
        univ = {}
        r = {}

2. The transitive property can be removed.
   Relation satisfying the remaining properties:
        univ = {a,b}
        r = {(a,b), (b,a)}

3. The irreflexive property can be removed.
   Relation satisfying the remaining properties:
        univ = {a,b}
        r = {(a,a),(b,b)}

No other individual property can be removed such that the remaining properties
are satisfied.

-------------------------------------------------------------------------------

Distributivity of Join
(solution by Michael Craig)

Proof for part a) was not necessary.

a) Distributivity of join over union holds: for a set s and relations p and q,
   suppose (A0) is in s.(p+q). Then for some AX,  (AX) is in s and (AX,A0) is
   in p or q, or both. Then (A0) is in  either s.p or s.q, or both, so it is
   certainly in s.p + s.q.

   Now assume (A0) is in s.p + s.q. Then for some (AX) in s, (AX,A0) is in
   either p or q. Thus (AX,A0) is certainly in p+q, so that s.(p+q) must
   contain (A0).

   In other words, for any atom A0, A0 is in s.(p+q) iff it is in s.p + s.q.

b) Distributivity of join over difference does not hold: consider the set s =
   {(A0,A1)} and the relations p = {(A0,A1)} and q = {(A1,A1)}. Then s.(p-q) =
   s.({(A0,A1)}) = {(A1)}, but s.p - s.q = {(A1)} - {(A1)} = {}.

c) Distributivity of join over intersection does not hold: consider the set s =
   {(A0),(A1)} and the relations p = {(A0,A0)} and q = {(A1,A0)}. Then s.(p&q)
   = s.({}) = {}, but s.p & s.q = {(A0)} & {(A0)} = {(A0)}.

-------------------------------------------------------------------------------

Modeling the Tube
(solution by Greg Dennis)

There are multiple equivalent constraints. If you found different solutions,
you can use the Alloy Analyzer to test whether they are equivalent.

a) named stations are on exactly the lines as shown in graphic
  Stanmore in (JubileeStation - CentralStation) - CircleStation
  BakerStreet in (JubileeStation & CircleStation) - CentralStation
  Epping in (CentralStation - JubileeStation) - CircleStation

b) no station (including those unnamed) is on all three lines
  no (JubileeStation & CentralStation & CircleStation)

c) the Circle line forms a circle
  all s: CircleStation {
    one s.circle
    CircleStation in s.^circle
  }

d) Jubilee is a straight line starting at Stanmore
  JubileeStation in Stanmore.*jubilee
  all s: JubileeStation {
    lone s.jubilee
    s not in s.^jubilee
  }

e) there's a station between Stanmore and BakerStreet
  let reach = ^jubilee | some Stanmore.reach & reach.BakerStreet

f) it is possible to travel from BakerStreet to Epping
  Epping in BakerStreet.^(jubilee + central + circle)