Download
language Essence 1.3
$ Ramsey's theorem
$ Decide if a complete graph K_n with edges coloured with c colours must have a monochromatic triangle
$ Keeps edges in both directions
given n : int(1..20)
given colours : int(1..10)
letting num_edges be (n * (n-1))
$ could made these an unamed type
letting Colour be domain int(1..colours)
letting Vertex be domain int(1..n)
find graph : relation (size num_edges) of ( Colour * Vertex * Vertex )
such that
$ make sure the it's a complete graph
forAll i : Vertex .
|(toSet(graph(_,i,_) ))| = (n - 1) /\
|(toSet(graph(_,_,i) ))| = (n - 1) /\
|(toSet(graph(_,i,i) ))| = 0,
forAll i, j : Vertex , j > i .
|(toSet(graph(_,i,j) ))| = 1 /\
|(toSet(graph(_,j,i) ))| = 1 /\
graph(_,i,j) = graph(_,j,i),
$ check for a monochromatic triangle
forAll i : Vertex .
forAll (c,e1) in toSet(graph(_, i, _) ) .
forAll tuple (t) in toSet(graph(c, i, _) ) , t != e1 .
!graph(c, t, e1)