| products/sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: ramsey_new.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
ramsey_new[T: TYPE]: THEORY
BEGIN IMPORTING graphs[T], subgraphs[T] i, j: VAR T n, p, q, ii: VAR nat % g: VAR graph[T] g: VAR graph[T] V: VAR finite_set[T] contains_clique(g, n): bool = (EXISTS (C: finite_set[T]): subset?(C,vert(g)) AND card(C) >= n AND (FORALL i,j: i/=j AND C(i) AND C(j) IMPLIES edge?(g)(i,j))) contains_indep(g, n): bool = (EXISTS (D: finite_set[T]): subset?(D, vert(g)) AND card(D) >= n AND (FORALL i, j: i/=j AND D(i) AND D(j) IMPLIES NOT edge?(g)(i, j))) subgraph_clique: LEMMA (FORALL (V: set[T]): contains_clique(subgraph(g, V), p) IMPLIES contains_clique(g, p)) subgraph_indep : LEMMA (FORALL (V: set[T]): contains_indep(subgraph(g, V), p) IMPLIES contains_indep(g, p)) G: VAR Graph[T] % finite and nonempty r1(G): finite_set[T] = (LET v0 = choose(vert(G)) IN { n: T | vert(G)(n) AND n /= v0 AND edge?(G)(v0,n)}) r2(G): finite_set[T] = (LET v0 = choose(vert(G)) IN { n: T | vert(G)(n) AND n /= v0 AND NOT edge?(G)(v0,n)}) SG1(G): graph[T] = subgraph(G, r1(G)) SG2(G): graph[T] = subgraph(G, r2(G)) v0: VAR nat card_r1_r2: LEMMA card(r1(G)) + card(r2(G)) >= size(G) - 1 % ramsey(p, q): RECURSIVE posnat = % (IF p=0 % THEN 1 % ELSIF q=0 % THEN 1 % ELSE (ramsey(p-1,q)+ramsey(p, q-1)) % ENDIF) % MEASURE p+q ramsey(p, q): posnat l1,l2: VAR nat ramsey_lem: LEMMA (FORALL l1,l2: l1+l2=ii IMPLIES (EXISTS (n: posnat): (FORALL (G: Graph[T]): size(G) >= n IMPLIES (contains_clique(G, l1) OR contains_indep(G, l2))))) ramseys_theorem: THEOREM (EXISTS (n: posnat): (FORALL (G: Graph[T]): size(G) >= n IMPLIES (contains_clique(G, l1) OR contains_indep(G, l2)))) END ramsey_new ¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
