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}