 |
 |
Forum zwiazane z depresją
wsparcie w depresji
|
|
|
|
|
|
|
|
|
|
|
starypustelnik
Junior
Dołączył: 14 Lut 2007
Posty: 91
Przeczytał: 0 tematów
Ostrzeżeń: 0/5
|
 Wysłany: Pią 14:22, 01 Lut 2008 Temat postu: Zaczepnie :D Raki |
 |
|
Panowie czytamy od tylu, Panie od przodu 
Jan Kochanowski Raki
Folgujmy paniom nie sobie, ma rada;
Miłujmy wiernie nie jest w nich przysada.
Godności trzeba nie za nic tu cnota,
Miłości pragną nie pragną tu złota.
Miłują z serca nie patrzają zdrady,
Pilnują prawdy nie kłamają rady.
Wiarę uprzejmą nie dar sobie ważą,
W miarę nie nazbyt ciągnąć rzemień każą.
Wiecznie wam służę nie służę na chwilę,
Bezpiecznie wierzcie nierad ja omylę.
czekam na rpioste (nie brać na serio :d)
Ostatnio zmieniony przez starypustelnik dnia Pią 14:26, 01 Lut 2008, w całości zmieniany 4 razy
|
|
| |
|
|
|
|
|
|
|
|
|
 |
|
code
Forumowicz
Dołączył: 03 Gru 2007
Posty: 117
Przeczytał: 0 tematów
Ostrzeżeń: 0/5
Skąd: z Apteki
|
| Wysłany: Pią 18:30, 01 Lut 2008 Temat postu: |
|
|
4 razy zmieniane ??
|
|
| |
|
|
|
|
|
|
|
|
starypustelnik
Junior
Dołączył: 14 Lut 2007
Posty: 91
Przeczytał: 0 tematów
Ostrzeżeń: 0/5
|
| Wysłany: Pią 20:24, 01 Lut 2008 Temat postu: |
|
|
|
ee bo sie czcionką bawiłem
|
|
| |
|
|
|
|
|
|
|
|
mala_nadzieja
Gość
|
| Wysłany: Pią 23:19, 01 Lut 2008 Temat postu: |
|
|
|
Pustelnik od tego masz podgląd
|
|
| |
|
|
|
|
|
|
|
|
Gość
|
| Wysłany: Sob 0:35, 02 Lut 2008 Temat postu: |
|
|
|
i to jest informatyk
|
|
| |
|
|
|
|
|
|
|
|
code
Forumowicz
Dołączył: 03 Gru 2007
Posty: 117
Przeczytał: 0 tematów
Ostrzeżeń: 0/5
Skąd: z Apteki
|
| Wysłany: Sob 0:42, 02 Lut 2008 Temat postu: |
|
|
| szumi89 napisał: |
| i to jest informatyk |
xD ciiii
|
|
| |
|
|
|
|
|
|
|
|
starypustelnik
Junior
Dołączył: 14 Lut 2007
Posty: 91
Przeczytał: 0 tematów
Ostrzeżeń: 0/5
|
| Wysłany: Sob 20:09, 02 Lut 2008 Temat postu: |
|
|
| Kod: |
infix 6 **;
infix 5 ++;
datatype prop = At of string (* atom *)
| !! of prop (* negacja *)
| ++ of prop * prop (* alternatywa - suma *)
| ** of prop * prop (* koniunkcja - iloczyn *)
| T
| F;
val p = At "p"; val q = At "q"; val r = At "r";
(* p+q*r *) val tw = p ++ q ** r;
infix 4 --> ;
fun p --> q = !!p ++ q;
infix 4 <=> ;
fun p<=>q = p ** q ++ !!p ** !! q;
fun nnf (At a) = At a
| nnf (!!(At a)) = !!(At a)
| nnf (!!T) = F
| nnf (!!F) = T
| nnf T = T
| nnf F = F
| nnf (!!(!! p)) = nnf p (* podwojna negacja *)
| nnf (!!((p++q))) = nnf (!!p ** !!q) (* negacja sumy = iloczyn negacji *)
| nnf (!!((p**q))) = nnf (!!p ++ !!q)
| nnf (p**q) = (nnf p) ** (nnf q) (* przetwarzanie elementow Kon *)
| nnf (p++q) = (nnf p) ++ (nnf q);
fun roz(p,q**r) = roz(p,q) ** roz(p,r) (* p+q*r = (p+q)*(p+r) *)
| roz(q**r,p) = roz(q,p) ** roz(r,p) (* q*r+p = (q+p)*(r+p) *)
| roz(p,q) = p ++ q ; (* zaden skladnik nie jest iloczynem *)
fun cnf (p ++ q) = roz(cnf p , cnf q) (* Alt zastapione przez roz (j.w.) *)
| cnf (p ** q) = (cnf p) ** (cnf q) (* rozklad skladnikow iloczynu *)
| cnf p = p; (* pojedynczy atom lub stala *)
exception NieCNF; (* wyrazenie nie przeksztalcone do CNF *)
fun pos (At a) = [a]
| pos (!! (At _)) = []
| pos (p++q) = pos p @ pos q
| pos T = []
| pos F = []
| pos _ = raise NieCNF;
fun neg (At _) = []
| neg (!! (At a)) = [a]
| neg (p ++ q) = neg p @ neg q
| neg T = []
| neg F = []
| neg _ = raise NieCNF;
infix mem;
fun x mem [] = false
| x mem (y::l) = (x=y) orelse (x mem l);
(* czesc wspolna dwu list *)
fun inter ([],ys)=[]
| inter (x::xs,ys) = if x mem ys then x::inter(xs,ys)
else inter(xs,ys);
fun chk_alt (T) = true
| chk_alt(p++q) = (chk_alt p) orelse (chk_alt q)
| chk_alt _ = false;
fun taut (p**q) = taut p andalso taut q (* p,q - czynniki Kon *)
| taut p = (chk_alt p) orelse ([] <> inter(pos p, neg p)); (* czesc wspolna powinna
byc NIEPUSTA *)
fun check(s) = taut (cnf (nnf (s))); (* zbiorcza funkcja *)
(* przekształcenie do postaci tekstowej *)
fun prop_toString (At x) = x
| prop_toString (!!(At x)) = ( "(!!" ^ x ^ ")")
| prop_toString (!!T) = ("(!!"^"T"^ ")")
| prop_toString (!!F) = ("(!!"^"F"^ ")")
| prop_toString (T) = ("(T"^ ")")
| prop_toString (F) = ("(F"^ ")")
| prop_toString (!!(p)) = "(!!"^ (prop_toString p) ^ ")"
| prop_toString ( p ++ q ) = ("(" ^ (prop_toString p) ^ ") ++ (" ^ (prop_toString q) ^ ")")
| prop_toString ( p ** q ) = ("(" ^ (prop_toString p) ^ ") ** (" ^ (prop_toString q) ^ ")");
(* Punkt P1 *)
val p = At "p" and q = At "q";
val tw = p ** q --> (p ++ q);
check tw;
(* Punkt P2.A *)
val tw = p ++ !! (p ** !!(p ++ q));
check tw;
(* Punkt P2.B *)
val wz1 = p <=> q;
val wz2 = (p-->q) ** (q-->p);
val tw = wz1 <=> wz2;
check tw;
(* Punkt P3 *)
(* realizacja bool *)
(* funkcje biblioteczne *)
fun OR(x1,x2) = x1 orelse x2;
fun AND(x1,x2) = x1 andalso x2;
fun NOT(x) = not x;
(* funkcja sterujaca *)
fun start_stop(start, stan, stop) =
let val y1 = OR(start,stan)
val y2 = NOT(stop)
val y3 = AND(y1,y2);
in y3 end;
(* wywolanie *)
val out = start_stop(true, false, false);
(* realizacja symboliczna *)
(* definicja atomów *)
val START = At "start" and STOP = At "stop" and STAN = At "stan";
(* funkcje symboliczne *)
fun OR_S(X1,X2) = X1++X2;
fun AND_S(X1,X2) = X1**X2;
fun NOT_S(X) = !!X;
(* symboliczne wykonanie *)
val Y1=OR_S(START,STAN);
val Y2=NOT_S(STOP);
val Y3 = AND_S(Y1,Y2);
val OUT = Y3;
(* specyfikacja symboliczna *)
val SPEC_OUT = (START ++ STAN) ** !! STOP;
(* twierdzenie o rownowaznosci *)
val tw = SPEC_OUT <=> OUT;
(* weryfikacja *)
check tw;
(* Punkt P4.1 *)
fun mux4(s0,s1,x0,x1,x2,x3) =
if not s0 andalso not s1 then x0
else if s0 andalso not s1 then x1
else if not s0 andalso s1 then x2
else x3;
(* realizacja symboliczna *)
fun OR4_S(X1,X2,X3,X4) = X1 ++ X2 ++ X3 ++ X4;
fun AND3_S(X1,X2,X3) = X1 ** X2 ** X3;
fun MUX4_S(S0,S1,X0,X1,X2,X3) =
OR4_S(
AND3_S(!! S0, !!S1, X0),
AND3_S( S0, !!S1, X1),
AND3_S(!! S0, S1, X2),
AND3_S( S0, S1, X3)
);
(* realizacja symboliczna funkcji z rys.3 *)
val A = At "A" and B = At "B" and C = At "C";
val uklad = MUX4_S(B, A, F, T, C, !!C);
(* specyfikacja *)
val spec = A ** B ** !!C ++ A ** !!B ** C ++ !!A ** B;
(* twierdzenie *)
val tw = uklad <=> spec;
(* sprawdzenie *)
check tw;
(* realizacja symboliczna funkcji z rys.4 *)
val A = At "A" and B = At "B" and C = At "C" and D = At "D";
fun NAND_S(X1,X2) = !! (X1 ** X2); (* definicja funkcji NAND *)
val Y1 = NAND_S(!!C,D);
val Y = MUX4_S(B, A, F, Y1, !!C, Y1);
(* specyfikacja *)
val spec = A ** B ** C ** D ++ !!A ** B ** C ** D ++
!!A ** B ** !!C ** !!D ++ !!A ** B ** C ** !!D ++
A ** !!B ** !!C ** !!D ++ A ** !!B ** !!C ** D ++
A ** B ** !!C ** !!D ++ A ** B ** C ** !!D ;
(* twierdzenie *)
val tw = Y <=> spec;
(* check tw; *)
(* check (spec <=> spec); *) (* 45 sekund *)
val tw' = prop_toString tw;
print tw';
val tw' = prop_toString spec;
print tw';
� |
|
|
| |
|
|
|
|
|
|
|
|
mala_nadzieja
Gość
|
| Wysłany: Sob 20:44, 02 Lut 2008 Temat postu: |
|
|
|
fajnie, że wiem o co chodzi
|
|
| |
|
|
|
|
|
|
|
|
Irmina
Junior
Dołączył: 13 Gru 2007
Posty: 90
Przeczytał: 0 tematów
Ostrzeżeń: 0/5
|
| Wysłany: Nie 20:19, 03 Lut 2008 Temat postu: |
|
|
|
eeee?
|
|
| |
|
|
|
|
|
|
|
|
Gość
|
| Wysłany: Pon 0:36, 04 Lut 2008 Temat postu: |
|
|
|
gdzie jak gdzie ale pod Kochanowskim to wklejac? ;p
|
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Nie możesz pisać nowych tematów
Nie możesz odpowiadać w tematach
Nie możesz zmieniać swoich postów
Nie możesz usuwać swoich postów
Nie możesz głosować w ankietach
|
|
|
|
