15 lines
486 B
Python
15 lines
486 B
Python
input: vertex/1, edge/2, color/1.
|
|
|
|
output: color/2.
|
|
|
|
# edge/2 is a set of pairs of vertices
|
|
assume: forall X, Y (edge(X,Y) -> vertex(X) and vertex(Y)).
|
|
|
|
# color/2 is a function from vertices to colors
|
|
spec: forall X, Z (color(X,Z) -> vertex(X) and color(Z)).
|
|
spec: forall X (vertex(X) -> exists Z color(X,Z)).
|
|
spec: forall X, Z1, Z2 (color(X,Z1) and color(X,Z2) -> Z1 = Z2).
|
|
|
|
# adjacent vertices have different colors
|
|
spec: not exists X, Y, Z (edge(X,Y) and color(X,Z) and color(Y,Z)).
|