\section{Normal Forms}
\bc\begin{verbatim}
module NF
where
import Form
import Hylotab
\end{verbatim}\ec
Function \verb^fuseLists^ will be used to keep the literals in the
clauses ordered.
\bc\begin{verbatim}
fuseLists :: Ord a => [a] -> [a] -> [a]
fuseLists [] ys = ys
fuseLists xs [] = xs
fuseLists (x:xs) (y:ys) | x < y = x:(fuseLists xs (y:ys))
| x == y = x:(fuseLists xs ys)
| x > y = y:(fuseLists (x:xs) ys)
\end{verbatim}\ec
\bc\begin{verbatim}
disjList :: [Form] -> [Form]
disjList [] = [Bool False]
disjList [fm] = [fm]
disjList (fm:fms) = map (disj fm) (disjList fms)
where
disj (Disj fms) (Disj fms') = Disj (fuseLists fms fms')
disj (Disj fms) fm = Disj (fuseLists fms [fm])
disj fm (Disj fms) = Disj (fuseLists [fm] fms)
disj fm fm' = Disj [fm,fm']
\end{verbatim}\ec
Negation normal form: like negation normal form for modal logic,
except for the case that we also apply the following rules:
\[
\Ibox{i} (\phi_1 \land \cdots \land \phi_n) \Rightarrow
(\Ibox{i} \phi_1 \land \cdots \land \Ibox{i} \phi_n)
\]
\[
\Icbox{i} (\phi_1 \land \cdots \land \phi_n) \Rightarrow
(\Icbox{i} \phi_1 \land \cdots \land \Icbox{i} \phi_n)
\]
\[
\downarrow x. (\phi_1 \land \cdots \land \phi_n) \Rightarrow
(\downarrow x. \phi_1 \land \cdots \land \downarrow x. \phi_n)
\]
\bc\begin{verbatim}
nnf :: Form -> [Form]
nnf (Bool True) = []
nnf (Neg (Bool True)) = [Bool False]
nnf (Bool False) = [Bool False]
nnf (Neg (Bool False)) = []
nnf (Nom nom) = [Nom nom]
nnf (Neg (Nom nom)) = [Neg (Nom nom)]
nnf (Prop prop) = [Prop prop]
nnf (Neg (Prop prop)) = [Neg (Prop prop)]
nnf (Conj fms) = concat (map nnf fms)
nnf (Neg (Conj fms)) = disjList (map Neg fms)
nnf (Disj fms) = disjList fms
nnf (Neg (Disj fms)) = concat (map nnf (map Neg fms))
nnf (Impl fm fm') = nnf (Disj [Neg fm,fm'])
nnf (Neg (Impl fm fm')) = nnf (Conj [fm,Neg fm'])
nnf (A fm) = map A (nnf fm)
nnf (Neg (A fm)) = map E (nnf (Neg fm))
nnf (E fm) = map E (nnf fm)
nnf (Neg (E fm)) = map A (nnf (Neg fm))
nnf (Box rel fm) = map (\x -> (Box rel x)) (nnf fm)
nnf (Neg (Box rel fm)) = [Dia rel (Conj (nnf (Neg fm)))]
nnf (Dia rel fm) = [Dia rel (Conj (nnf fm))]
nnf (Neg (Dia rel fm)) = map (\x -> (Box rel x)) (nnf (Neg fm))
nnf (Cbox rel fm) = map (\x -> (Cbox rel x)) (nnf fm)
nnf (Neg (Cbox rel fm)) = [Cdia rel (Conj (nnf (Neg fm)))]
nnf (Cdia rel fm) = [Cdia rel (Conj (nnf fm))]
nnf (Neg (Cdia rel fm)) = map (\x -> (Cbox rel x)) (nnf (Neg fm))
nnf (At nom fm) = map (\x -> (At nom x)) (nnf fm)
nnf (Neg (At nom fm)) = map (\x -> (At nom x)) (nnf (Neg fm))
nnf (Down v fm) = map (\x -> (Down v x)) (nnf fm)
nnf (Neg (Down v fm)) = map (\x -> (Down v x)) (nnf (Neg fm))
nnf (Neg (Neg fm)) = nnf fm
\end{verbatim}\ec
\bc\begin{verbatim}
compress :: Form -> Form
compress (At k (At n fm)) = compress (At n fm)
compress (At k fm) = At k (compress fm)
compress (A (A fm)) = compress (A fm)
compress (A (E fm)) = compress (E fm)
compress (E (E fm)) = compress (E fm)
compress (E (A fm)) = compress (A fm)
compress (A fm) = A (compress fm)
compress (E fm) = E (compress fm)
compress (Neg fm) = Neg (compress fm)
compress (Box rel fm) = Box rel (compress fm)
compress (Dia rel fm) = Dia rel (compress fm)
compress (Cbox rel fm) = Cbox rel (compress fm)
compress (Cdia rel fm) = Cdia rel (compress fm)
compress (Down v fm) = Down v (compress fm)
compress fm = fm
\end{verbatim}\ec
\bc\begin{verbatim}
nf :: Form -> [Form]
nf fm = map compress (nnf fm)
\end{verbatim}\ec