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)