мета-данные страницы
Загрузка не удалась. Возможно, проблемы с правами доступа?
no way to compare when less than two revisions
Различия
Показаны различия между двумя версиями страницы.
— | haskell:sekv [17/04/2013 19:01] (текущий) – создано vlasov | ||
---|---|---|---|
Строка 1: | Строка 1: | ||
+ | <code haskell> | ||
+ | data LogicFormula = A|B|C|D|E|F|G|H|I|J|K|L|M|N| | ||
+ | | ||
+ | | ||
+ | | ||
+ | Neg LogicFormula deriving (Eq, | ||
+ | data Sekv = [LogicFormula] :- [LogicFormula] deriving (Eq, | ||
+ | aks :: Sekv -> Bool | ||
+ | aks ([x] :- [y]) = if x == y then True else False | ||
+ | ax w = if (aks w) then w else error "w is not an axiom!" | ||
+ | |||
+ | p1 (g :- [x]) (g2 :- [y]) | g==g2 = g :- [x :&: y] | ||
+ | | otherwise = error "g != g2" | ||
+ | p2 (g :- [x :&: y]) = g :- [x] | ||
+ | p3 (g :- [x :&: y]) = g :- [y] | ||
+ | p4 (g :- [x]) y = g :- [x :+: y] | ||
+ | p5 (g :- [y]) x = g :- [x :+: y] | ||
+ | p6 ((z1:g1) :- [y1]) | ||
+ | ((x2:g2) :- [y2]) | ||
+ | (g3 :- [z3:+:x3]) | g1==g3 && g1==g3 && | ||
+ | y1==y2 && z1==z3 && x2==x3 = g1 :- [y1] | ||
+ | | otherwise = error "with =" | ||
+ | p7 ((x:g) :- [y]) = g :- [(x: | ||
+ | p8 (g :- [x]) (g2 :- [x2: | ||
+ | | otherwise = error "g!=g2 or x!=x2" | ||
+ | p9 (((Neg x):g) :- []) = g :- [x] | ||
+ | p10 (g :- [x]) (g2 :- [x2]) | g==g2 && x==x2 = g :- [] | ||
+ | | otherwise = error "g!=g2 or x!=x2" | ||
+ | p11 (g :- x) n = Tr_inList g n where | ||
+ | | ||
+ | (x1s, | ||
+ | |||
+ | p12 (g :- x) y = (y:g) :- x | ||
+ | </ |