Type :? for help
Prelude>
Prelude> :l "E:\\haskell\\alcn.hs"
Main> subsumes Top Top []
True
Main> subsumes Top (Not Top) []
True
Main> subsumes (Not Top) Top []
False
Main> subsumes (Not Top) (Not Top) []
True
Main> subsumes (Atomic "A") (Atomic "B") []
False
Main> subsumes (Atomic "A") (Atomic "B") [Atomic "B" `Implies` Atomic "A"]
True
Main> subsumes (Atomic "A") (Atomic "B") [Atomic "A" `Implies` Atomic "B"]
False
Main> disjoint (Not (Atomic "A")) (Atomic "B") []
False
Main> disjoint (Not (Atomic "A")) (Atomic "B") [Atomic "B" `Implies` Atomic "A"]
True
Main> disjoint (Not (Atomic "A")) (Atomic "A") []
True
Main> disjoint (Not ((Atomic "A") `And` (Atomic "B"))) (Atomic "A") []
False
Main> disjoint ((Not (Atomic "A")) `And` (Atomic "B")) (Atomic "A") []
True
Main> subsumes (Exists "gyereke" (Atomic "Okos" `And` Atomic "Szep")) 
((Exists "gyereke" (Atomic "Okos")) `And` (Exists "gyereke" (Atomic "Szep")) ) []
False
Main> subsumes (Exists "gyereke" (Atomic "Okos" `Or` Atomic "Szep")) 
((Exists "gyereke" (Atomic "Okos")) `And` (Exists "gyereke" (Atomic "Szep")) ) []
True 
Main> nnf (Not (Exists "gy" ((Atomic "Okos") `And` (Not (Atomic "Szep")))))
All "gy" (Not (Atomic "Okos") `Or` Atomic "Szep") 
Main> equivalent (Atomic "A") (Atomic "B") [(Atomic "A") `Implies` (Atomic "B")]
False
Main> equivalent (Atomic "A") (Atomic "B") [(Atomic "A") `Implies` (Atomic "B"), (Not
(Atomic "A")) `Implies` (Not (Atomic "B"))]
True
Main> equivalent (Atomic "A") (Atomic "B") [(Atomic "A") `Implies` (Atomic "B"), (Atom
ic "B") `Implies` (Atomic "A")]
True
Main> satisfiable (Atomic "A") [Top `Implies` (Not Top)]
False
Main> satisfiable Top [Top `Implies` (Not Top)]
False
Main> satisfiable Top []
True
Main> satisfiable (Atomic "A") []
True   
Main> consistent [Top `Implies` (Not Top)]
False