The module for formulas imports the standard \verb^List^ module: 

\begin{code}
module Form where 
import List
\end{code}

Identifiers for constant, variable, and tableau parameter nominals
are integers. Indices for relations and basic propositions are integers.

\begin{code}
type Id   = Integer 
type Rel  = Integer
type Prop = Integer 
\end{code}

Nominals can be constants, new parameters (constant nominals added
during the tableau development process), or variables. We will need 
a linear ordering on nominals, so we instruct the Haskell system to 
derive \verb^Ord^ for the datatype. 

\begin{code}
data Nom = C Id | N Id | V Id deriving (Eq,Ord)
\end{code}

Declare \verb^Nom^ as an instance of the \verb^Show^ class: 

\begin{code}
instance Show Nom where 
   show (C n) = 'c': show n 
   show (V n) = 'x': show n
   show (N n) = 'n': show n
\end{code} 

Formulas according to 
\begin{eqnarray*}
\phi & ::= & \top \mid \bot \mid p \mid n \mid x \mid \neg \phi 
  \mid \bigwedge_i\phi_i \mid \bigvee_i \phi_i \mid \phi \rightarrow \phi' 
   \mid \\
     &     & A \phi \mid E \phi \mid \Ibox{i} \phi \mid 
             \Icbox{i}\phi \mid \Idia{i} \phi 
             \mid \Icdia{i} \phi  \mid 
             @ n \phi \mid \downarrow\! x. \phi
\end{eqnarray*}

The datatype \verb^Form^ defines formulas.

\begin{code}
data Form =  Bool Bool
           | Prop Prop
           | Nom  Nom
           | Neg  Form
           | Conj [Form]
           | Disj [Form]
           | Impl Form Form
           | A    Form
           | E    Form
           | Box  Rel Form
           | Cbox Rel Form
           | Dia  Rel Form 
           | Cdia Rel Form 
           | At   Nom Form
           | Down Id Form
     deriving (Eq,Ord)
\end{code}

Declare \verb^Form^ as an instance of the \verb^Show^ class: 

\begin{code} 
instance Show Form where 
   show (Bool True)         = "T"
   show (Bool False)        = "F"
   show (Prop i)            = 'p':show i
   show (Nom i)             = show i
   show (Neg f)             = '-' : show f
   show (Conj [])           = "T" 
   show (Conj [f])          = show f
   show (Conj (f:fs))       =  "(" ++ show f ++ " & " ++ showCtail fs ++ ")"
     where showCtail []     = ""
           showCtail [f]    = show f
           showCtail (f:fs) = show f ++ " & " ++ showCtail fs
   show (Disj [])           = "F" 
   show (Disj [f])          = show f
   show (Disj (f:fs))       =  "(" ++ show f ++ " v " ++ showDtail fs ++ ")"
     where showDtail []     = ""
           showDtail [f]    = show f
           showDtail (f:fs) = show f ++ " v " ++ showDtail fs
   show (Impl f1 f2)        = "(" ++ show f1 ++ " -> " ++ show f2 ++ ")"
   show (A f)               = 'A' : show f
   show (E f)               = 'E' : show f
   show (Box name f)        = "[" ++ show name ++ "]" ++ show f
   show (Cbox name f)       = "[" ++ show name ++ "~]" ++ show f
   show (Dia name f)        = "<" ++ show name ++ ">" ++ show f
   show (Cdia name f)       = "<" ++ show name ++ "~>" ++ show f
   show (At nom f)          = '@': show nom ++ show f
   show (Down i f)          = "Dx" ++ show i ++ "." ++ show f
\end{code}

Flatten conjunctions: 

\begin{code}
flattenConj :: [Form] -> [Form]
flattenConj []                = []
flattenConj ((Conj conjs):fs) = flattenConj conjs ++ flattenConj fs
flattenConj ( f          :fs) = f : (flattenConj fs)
\end{code}

Flatten disjunctions: 

\begin{code}
flattenDisj :: [Form] -> [Form]
flattenDisj []                = []
flattenDisj ((Disj disjs):fs) = flattenDisj disjs ++ flattenDisj fs
flattenDisj ( f          :fs) = f : (flattenDisj fs)
\end{code}

For parsing, it is convenient to have various types for lists of
formulas:

\begin{code}
type Forms  = [Form]
type Conjs  = [Form]
type Disjs  = [Form]
\end{code}

\section{Normal Forms}

Function \verb^fuseLists^ will be used to keep the components of 
a formula ordered. 

\begin{code}
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{code}

\verb^disjList^ maps a disjunction of formulas to an equivalent 
conjunction of formulas. 

\begin{code}
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{code}
  
Negation normal form: like negation normal form for modal logic, 
except for the case that we also apply the following rules: 
\[ 
A (\phi_1 \land \cdots \land \phi_n) \Rightarrow 
  (A \phi_1 \land \cdots \land A \phi_n) 
\]
\[ 
\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) 
\]
\[
@ n (\phi_1 \land \cdots \land \phi_n) \Rightarrow 
  (@ n \phi_1 \land \cdots \land @ n \phi_n) 
\]
\[
@ n (\phi_1 \lor \cdots \lor \phi_n) \Rightarrow 
  (@ n \phi_1 \lor \cdots \lor @ n \phi_n) 
\]

\begin{code}
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) = nnfs fms 
nnf (Neg (Conj fms)) = disjList (map Neg fms)
nnf (Disj fms) = disjList fms
nnf (Neg (Disj fms)) = nnfs (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 (Disj fms)) = [Disj (nnfs (map (\x -> (At nom x)) fms))]
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{code}

Put a list of formulas in negation normal form: 

\begin{code}
nnfs :: [Form] -> [Form]
nnfs = concat . (map nnf)
\end{code}

Compress a formula by removing redundant occurrences of $A$, $E$,
$@ n$. 

\begin{code}
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{code}

\begin{code}
nf :: Form -> [Form]
nf fm = map compress (nnf fm)
\end{code}