\documentclass[11pt]{article} \usepackage{url} \usepackage{latexsym,amssymb,amsmath,theorem,proof,calc,alltt} %\usepackage{parsetree} %\usepackage{tree-dvips} \usepackage{pst-tree} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % VERSION FEB 2002 % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \input{mymacros} \newcommand{\close}[1]{\begin{array}{c}{#1} \\ {\times} \end{array}} \newcommand{\clsubs}[2]{\begin{array}{c}{#1} \\ {#2} \end{array}} \newcommand{\stack}[1]{\begin{array}{c}{#1} \end{array}} \newcommand{\barr}{\begin{array}{c}} \newcommand{\earr}{\end{array}} \newcommand{\EQ}{\approx} \newcommand{\NEQ}{\not\approx} \newcommand{\var}{{\rm var\:}} %\newcommand{\dom}{{\rm dom\:}} %\newcommand{\rng}{{\rm rng\:}} \newcommand{\bB}{\mbox{\boldmath $B$}} \newcommand{\ttop}{\mbox{\boldmath $\top\!\!\!\!\top$}} \newcommand{\bbot}{\mbox{\boldmath $\bot\!\!\!\!\bot$}} \newcommand{\bT}{\mbox{\boldmath $T$}} \newcommand{\cB}{\mbox{$\cal B$}} \newcommand{\cE}{{\cal E}} \newcommand{\href}[1]{} \newcommand{\Nat}{\mathbb{N}} \newcommand{\Exists}{\boldsymbol{\exists\!\!\!\exists}} \newcommand{\Forall}{\boldsymbol{\forall\!\!\!\forall}} \newcommand{\Neg}{\boldsymbol{\neg\!\!\!\neg}} \newcommand{\SC}{\ \boldsymbol{;}\ } \newsavebox{\fminibox} \newlength{\fminilength} \newenvironment{fminipage}[1][\linewidth] {\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule-1em}% \bigskip\begin{lrbox}{\fminibox}\quad\begin{minipage}{\fminilength}\bigskip} {\smallskip\end{minipage}\end{lrbox}\noindent\fbox{\usebox{\fminibox}}\bigskip} \newcommand{\bc}{\begin{fminipage}} \newcommand{\ec}{\end{fminipage}} \newenvironment{code}{\begin{fminipage}\begin{alltt}}% {\end{alltt}\end{fminipage}} \newenvironment{pcode}{\begin{fminipage}\begin{alltt}}% {\end{alltt}\end{fminipage} } \renewcommand{\impl}{\Rightarrow} \newtheorem{exercise}[theorem]{Exercise} \newcommand{\produces}{\longrightarrow} \newcommand{\yields}{\Rightarrow} \setlength{\textheight}{22cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\parindent}{0 ex} \setlength{\parskip}{1.5 ex} \newcommand{\Ibox}[1]{[{\scriptstyle\:#1\: }]} \newcommand{\Idia}[1]{\langle{\scriptstyle\: #1\: }\rangle} \newcommand{\Icbox}[1]{[{\scriptstyle\: #1\:}]^{\:\breve{}}} \newcommand{\Icdia}[1]{\langle{\scriptstyle\: #1\: }\rangle^{\breve{}}} \newcommand{\Cbox}{\Box^{\:\breve{}}} \newcommand{\Cdia}{\Diamond^{\breve{}}} \title{HyLoTab --- Tableau-based Theorem Proving for Hybrid Logics} \author{Jan van Eijck \\ \small\em CWI and ILLC, Amsterdam, Uil-OTS, Utrecht } \begin{document} \maketitle \begin{abstract} \noindent This paper contains the full code of a prototype implementation in Haskell \cite{Haskell98:rep}, in literate programming' style \cite{Knuth:lp}, of the tableau-based calculus and proof procedure for hybrid logic presented in \cite{Eijck02:cthl}. \end{abstract} \paragraph{Keywords:} Tableau theorem proving for hybrid logic, equality reasoning, model generation, implementation, Haskell, literate programming. \paragraph{MSC codes:} 03B10, 03F03, 68N17, 68T15 \section{Introduction} We aim for clarity of exposition rather than efficiency or clever coding.\footnote{And we wish more people would do that.} The program consists of the following modules: \begin{description} \item[Form] Describes the representation and handling of formulas. See section \ref{FormStart}. \item[HylotabLex] Describes lexical scanning for formulas. Code in the first appendix. \item[HylotabParse] The parsing module, generated by the Haskell parser generator {\em Happy}. The input for the parser generator is in the second appendix. \item[Hylotab] The module where tableau nodes and tableaux are defined, and where tableau expansion is implemented. See Sections \ref{TabStart} through \ref{TabStop}. \item[Main] A module for stand-alone (non-interactive) use of the proof engine. It contains a function \verb^main^ that interprets a command line parameter as a file name, reads a formula from the named file, and calls the \verb^sat^ function for the formula. Useful for generating compiled code. See Section \ref{SectMain}. \end{description} The code follows the Haskell'98 standard; it was tested with the Haskell interpreter {\em Hugs}\/ and with the GHC compiler in both interpret mode {\em ghci}, and compile mode {\em ghc}. {\em Hugs}\/ and {\em GHC}\/ run on most platforms. Program and documentation are freely available from the internet, for {\em Hugs}\/ from \url{http://www.haskell.org/hugs}, and for {\em GHC}\/ from \url{http://www.haskell.org/ghc}. \section{Version} This is the first version, written in January/February 2002. When this gets public, it will get version number $1.00$. \section{Datatype Declarations for Nominals and Formulas} \label{FormStart} \input{Form} \label{FormEnd} \section{Types for Tableau Development} \label{TabStart} First we declare the module for tableau development. It imports the standard \verb^List^ and \verb^IOExts^ modules, and it imports modules for lexical scanning and parsing. See the appendices for \verb^HylotabLex^ and \verb^HylotabParse^. The \verb^IOExts^ module is needed for tracing. \begin{code} module Hylotab where import List import IOExts import Form import HylotabLex import HylotabParse \end{code} Tableau nodes have indices to point at the next available fresh nominal for the node. \begin{code} type Index = Integer \end{code} Tableau nodes have domains: lists of all nominals occurring in the tableau: \begin{code} type Domain = [Nom] \end{code} \section{Collecting Nominals from Formulas} The following function adds an item to a list, but only in case the item is not yet present: \begin{code} add :: (Eq a) => a -> [a] -> [a] add x xs = if elem x xs then xs else (x:xs) \end{code} The following functions collect the constant nominals and the free occurrences of variable nominals from a formula or a formula list. \begin{code} nomsInForm :: Form -> [Nom] nomsInForm (Bool _) = [] nomsInForm (Prop _) = [] nomsInForm (Nom nom) = [nom] nomsInForm (Neg form) = nomsInForm form nomsInForm (Conj forms) = nomsInForms forms nomsInForm (Disj forms) = nomsInForms forms nomsInForm (Impl f1 f2) = nomsInForms [f1,f2] nomsInForm (A form) = nomsInForm form nomsInForm (E form) = nomsInForm form nomsInForm (Box _ form) = nomsInForm form nomsInForm (Dia _ form) = nomsInForm form nomsInForm (Cbox _ form) = nomsInForm form nomsInForm (Cdia _ form) = nomsInForm form nomsInForm (At nom form) = add nom (nomsInForm form) nomsInForm (Down id form) = filter (/= (V id)) (nomsInForm form) nomsInForms :: [Form] -> [Nom] nomsInForms = nub . concat. map nomsInForm \end{code} \section{Substitutions} We need to define the result of a substitution of a nominal for a nominal in nominals, in formulas, and in structures defined from those. Represent a substitution as a nominal/nominal pair. \begin{code} type Subst = (Nom,Nom) \end{code} Application of a substitution to a nominal: \begin{code} appNom :: Subst -> Nom -> Nom appNom (n,m) nom = if n == nom then m else nom \end{code} Application of a substitution to a domain. Note that the substitution may identify individuals, so after the substitutition we have to clean up the list with \verb^nub^ to remove possible duplicates. \begin{code} appDomain :: Subst -> Domain -> Domain appDomain = map . appNom \end{code} Application of a substitution to a list of \verb^(Nom,Nom)^ pairs: \begin{code} appNNs :: Subst -> [(Nom,Nom)] -> [(Nom,Nom)] appNNs b = map (\ (n,m) -> (appNom b n, appNom b m)) \end{code} Application of a substitution to a list of \verb^(Nom,Rel,Nom)^ triples: \begin{code} appNRNs :: Subst -> [(Nom,Rel,Nom)] -> [(Nom,Rel,Nom)] appNRNs b = map (\ (n,r,m) -> (appNom b n, r, appNom b m)) \end{code} Application of a substitution to a list of \verb^(Nom,PropName)^ pairs: \begin{code} appNPs :: Subst -> [(Nom,Prop)] -> [(Nom,Prop)] appNPs b = map (\ (n,name) -> (appNom b n, name)) \end{code} Application of a substitution to a formula or a formula list. Note that in the application of $(n,m)$ to a binder formula $\downarrow v . F$, the occurrences of $v$ inside $F$ are not changed. Substitutions only affect the {\em free}\/ variables of a formula, and the occurrences of $v$ inside $\downarrow v . F$ are {\em bound}. \begin{code} appF :: Subst -> Form -> Form appF b (Bool tv) = (Bool tv) appF b (Prop p) = (Prop p) appF b (Nom nom) = (Nom (appNom b nom)) appF b (Neg f) = Neg (appF b f) appF b (Conj fs) = Conj (appFs b fs) appF b (Disj fs) = Disj (appFs b fs) appF b (Impl f1 f2) = Impl (appF b f1) (appF b f2) appF b (A f) = A (appF b f) appF b (E f) = E (appF b f) appF b (Box r f) = Box r (appF b f) appF b (Dia r f) = Dia r (appF b f) appF b (Cbox r f) = Cbox r (appF b f) appF b (Cdia r f) = Cdia r (appF b f) appF b (At n f) = At (appNom b n) (appF b f) appF (C n,nom) (Down m f) = Down m (appF (C n,nom) f) appF (N n,nom) (Down m f) = Down m (appF (N n,nom) f) appF (V n,nom) (Down m f) | n == m = Down m f | otherwise = Down m (appF (V n,nom) f) appFs :: Subst -> [Form] -> [Form] appFs = map . appF \end{code} Application of a substitution to a list of \verb^(Nom,Rel,Form)^ triples: \begin{code} appNRFs :: Subst -> [(Nom,Rel,Form)] -> [(Nom,Rel,Form)] appNRFs b = map (\ (n,r,f) -> (appNom b n, r, appF b f)) \end{code} \section{Tableau Nodes and Tableaux} A node of a tableau consists of: \begin{enumerate} \item a tableau index (needed to generate fresh tableau parameters), \item a domain (all nominals occurring at the node), \item a list of nominal pairs to represent the $n \NEQ m$ constraints on the node, \item a list of $(n,i,m)$ triples to represent the $nR_im$ accessibilities on the node, \item a list of formulas $\phi$ to represent the $A \phi$ formulas that have been applied to all nominals in the domain of the node (the universal constraints of the node), \item a list of $(n,i,\phi)$ triples to represent the $@n \Ibox{i} \phi$ formulas of the node that have been combined with all the $nR_im$ accessibilities on the node (the boxed constraints of the node), \item a list of $(n,i,\phi)$ triples to represent the $@n \Icbox{i} \phi$ formulas of the node that have been combined with all the $mR_in$ accessibilities on the node (the converse boxed constraints of the node), \item a list of $(n,i)$ pairs to represent the positive atom attributions $@ n p_i$ on the node, \item a list of $(n,i)$ pairs to represent the negative atom attributions $@ n \neg p_i$ on the node, \item a list of pending formulas at the node (these are the formulas yet to be treated by the proof engine). \end{enumerate} \begin{code} data Node = Nd Index Domain [(Nom,Nom)] [(Nom,Rel,Nom)] [Form] [(Nom,Rel,Form)] [(Nom,Rel,Form)] [(Nom,Prop)] [(Nom,Prop)] [Form] deriving (Eq,Show) \end{code} A tableau is a list of its nodes: \begin{code} type Tableau = [Node] \end{code} \section{Formula Typology, Formula Decomposition} Code for recognizing $\alpha$ and $\beta$ formulas: \begin{code} alpha, beta :: Form -> Bool alpha (Conj _) = True alpha (Neg (Disj _)) = True alpha (Neg (Impl _ _)) = True alpha _ = False beta (Disj _) = True beta (Impl _ _) = True beta (Neg (Conj _)) = True beta _ = False \end{code} Code for recognizing $A$ and $E$ formulas: \begin{code} isA, isE :: Form -> Bool isA (A _) = True isA (Neg (E _)) = True isA _ = False isE (E _) = True isE (Neg (A _)) = True isE _ = False \end{code} Code for recognizing $\Box$, $\Cbox$, $\Diamond$, $\Cdia$ formulas: \begin{code} box, cbox, diamond, cdiamond :: Form -> Bool box (Box _ _) = True box (Neg (Dia _ _)) = True box _ = False cbox (Cbox _ _) = True cbox (Neg (Cdia _ _)) = True cbox _ = False diamond (Dia _ _) = True diamond (Neg (Box _ _)) = True diamond _ = False cdiamond (Cdia _ _) = True cdiamond (Neg (Cbox _ _)) = True cdiamond _ = False \end{code} Code for recognizing $\downarrow$, and $@$ formulas: \begin{code} down, label :: Form -> Bool down (Down _ _ ) = True down (Neg (Down _ _ )) = True down _ = False label (At _ _) = True label (Neg (At _ _)) = True label _ = False \end{code} Code for identifying the Boolean constants, the positive literals and the negative literals: \begin{code} isBool,plit, nlit :: Form -> Bool isBool (Bool _) = True isBool (Neg (Bool _)) = True isBool _ = False plit (Prop _) = True plit _ = False nlit (Neg (Prop _)) = True nlit _ = False \end{code} Code for identifying the nominals, the negated nominals, the access and converse access formulas and the double negations: \begin{code} isNom, ngNom, isAcc, isCacc, dneg :: Form -> Bool isNom (Nom _) = True isNom _ = False ngNom (Neg (Nom _)) = True ngNom _ = False isAcc (Dia _ (Nom _)) = True isAcc (Neg (Box _ (Neg (Nom _)))) = True isAcc _ = False isCacc (Cdia _ (Nom _)) = True isCacc (Neg (Cbox _ (Neg (Nom _)))) = True isCacc _ = False dneg (Neg (Neg f)) = True dneg _ = False \end{code} Function for getting the value of a Boolean constant from a formula: \begin{code} getBool :: Form -> Bool getBool (Bool b) = b getBool (Neg (Bool b)) = not b \end{code} Function for converting a literal (a propositional atom or a negation of a propositional atom) at a nominal $n$ to a pair consisting of the $n$ and the name of the atom. \begin{code} nf2np :: Nom -> Form -> (Nom,Prop) nf2np nom (Prop name) = (nom,name) nf2np nom (Neg (Prop name)) = (nom,name) \end{code} Function for converting a nominal $m$ or negated nominal $\neg m$, at a nominal $n$, to the pair $(n,m)$. \begin{code} nf2nn :: Nom -> Form -> (Nom,Nom) nf2nn n (Nom m) = (n,m) nf2nn n (Neg (Nom m)) = (n,m) \end{code} Function for getting the nominal out of a nominal formula, a negated nominal formula, or an access formula (a formula of the form $\Idia{i} m$, $\neg \Ibox{i} \neg m$, $\Icdia{i} m$ or $\neg \Icbox{i} \neg m$): \begin{code} getNom :: Form -> Nom getNom (Nom nom) = nom getNom (Neg (Nom nom)) = nom getNom (Dia _ (Nom nom)) = nom getNom (Neg (Box _ (Neg (Nom nom)))) = nom getNom (Cdia _ (Nom nom)) = nom getNom (Neg (Cbox _ (Neg (Nom nom)))) = nom \end{code} Function for getting the relation and the target nominal out of a box or diamond formula: \begin{code} getRel :: Form -> Rel getRel (Dia rel _) = rel getRel (Box rel _) = rel getRel (Neg (Dia rel _)) = rel getRel (Neg (Box rel _)) = rel getRel (Cdia rel _) = rel getRel (Cbox rel _) = rel getRel (Neg (Cdia rel _)) = rel getRel (Neg (Cbox rel _)) = rel \end{code} The components of a (non-literal) formula are given by: \begin{code} components :: Form -> [Form] components (Conj fs) = fs components (Disj fs) = fs components (Impl f1 f2) = [Neg f1,f2] components (Neg (Conj fs)) = map Neg fs components (Neg (Disj fs)) = map Neg fs components (Neg (Impl f1 f2)) = [f1,Neg f2] components (Neg (Neg f)) = [f] components (A f) = [f] components (Neg (A f)) = [Neg f] components (E f) = [f] components (Neg (E f)) = [Neg f] components (Box _ f) = [f] components (Neg (Box _ f)) = [Neg f] components (Cbox _ f) = [f] components (Neg (Cbox _ f)) = [Neg f] components (Dia _ f) = [f] components (Neg (Dia _ f)) = [Neg f] components (Cdia _ f) = [f] components (Neg (Cdia _ f)) = [Neg f] components (Down x f) = [f] components (Neg (Down x f)) = [Neg f] components (At nom f) = [f] components (Neg (At nom f)) = [Neg f] \end{code} Located components of a (non-literal) formula: \begin{code} lcomponents :: Nom -> Form -> [Form] lcomponents nom f = [At nom f' | f' <- components f ] \end{code} For label formulas, the following function returns the label: \begin{code} getLabel :: Form -> Nom getLabel (At nom _) = nom getLabel (Neg (At nom _)) = nom \end{code} For binder formulas, the following function returns the binder: \begin{code} binder :: Form -> Id binder (Down x f) = x binder (Neg (Down x f)) = x \end{code} Check a list of formulas for nominal contradiction. \begin{code} checkNom :: [Form] -> Bool checkNom fs = null [ m | (At n (Neg (Nom m))) <- fs, m == n ] \end{code} Check of a list of formulas for contradiction (not used now; but could be included in the definition of \verb^check^ below): \begin{code} checkFs :: [Form] -> Bool checkFs fs = all (\ (f,f') -> (f /= (Neg f') && (Neg f) /= f')) fpairs where fpairs = [ (f,f') | (At c f) <- fs, (At c' f') <- fs, c == c' ] \end{code} Checking a node for closure, with closure indicated by return of $[]$. \begin{code} check :: Node -> [Node] check nd@(Nd i dom neqs accs ufs boxes cboxes pos neg fs) = if (checkNN neqs) && (checkPN pos neg) && (checkNom fs) -- && (checkFs fs) then [nd] else [] where checkNN = all (\(m,n) -> m /= n) checkPN poss negs = (intersect poss negs) == [] \end{code} Sometimes we just have to check the final component of a node: \begin{code} checkNdNom :: Node -> [Node] checkNdNom nd@(Nd i dom neqs accs ufs boxes cboxes pos neg fs) = if (checkNom fs) then [nd] else [] \end{code} \section{Tableau Expansion} While expanding a tableau, it is convenient to prune branches as quickly as possible, by immediately removing closing nodes. Immediate closure is indicated by $[]$. Also, we should take care not to introduce duplicates into the nodes; the function \verb^nub^ cleans up lists by removing duplicates. We now turn to the treatment of an expansion step of a branch (node). This function is at the heart of the program: \begin{code} step :: Node -> Tableau \end{code} Applying an expansion step to a node $N$ yields a tableau, i.e., a list of nodes. If the expansion step results in closure of $N$, we return $[]$. Otherwise we return a non-empty list of open tableau nodes. If the function is called for a node $N$ with an empty pending formula list, there is nothing left to do, so we return $[N]$. \begin{code} step (Nd i dom neqs accs ufs boxes cboxes pos neg []) = check (Nd i dom neqs accs ufs boxes cboxes pos neg []) \end{code} If the list of pending formulas starts with a Boolean constant, then remove it if it is the constant \verb^True^, otherwise close the node: \begin{code} step (Nd i dom neqs accs ufs boxes cboxes pos neg ((At nom f):fs)) | isBool f = if getBool f then [Nd i dom neqs accs ufs boxes cboxes pos neg fs] else [] \end{code} The list of pending formulas starts with a propositional literal: check for closure; if the node does not close, then add the literal to the appropriate list. \begin{code} | plit f = let ni = nf2np nom f pos' = add ni pos in if elem ni neg then [] else [Nd i dom neqs accs ufs boxes cboxes pos' neg fs] | nlit f = let ni = nf2np nom f neg' = add ni neg in if elem ni pos then [] else [Nd i dom neqs accs ufs boxes cboxes pos neg' fs] \end{code} The list of pending formulas starts with a nominal. In this case we perform a substitution and check for closure. Note the following: \begin{itemize} \item Applying a substitution to a list of access relations may result in a {\em change}\/ in the access relations, and thus in a violation of a universal constraint, thus destroying the invariant that the universal constraints hold for all nominals present at the node. To restore that invariant, we have to take care that the universal constraints get (re-)applied to the new nominal that fuses two old ones. \item Applying a substitution to a list of access relations may result in new access relations, thus destroying the invariant that the box and converse box constraints of the node have been applied for all access relations of the node. To restore that invariant, we have to take care that all box and converse box constraints get applied to the new access relations. \item Applying a substitution to a list of box constraints may result in new box constraints, thus destroying the invariant that the box constraints of the node have been applied for all access relations of the node. To restore that invariant, we have to apply all new box constraints to all access relations of the node. \item Applying a substitution to a list of converse box constraints may result in new converse box constraints, thus destroying the invariant that the converse box constraints of the node have been applied for all access relations of the node. To restore that invariant, we have to apply all new converse box constraints to all access relations of the node. \end{itemize} \begin{code} | isNom f = if getNom f == nom then [Nd i dom neqs accs ufs boxes cboxes pos neg fs] else let k = getNom f m = min k nom n = max k nom dom' = nub (appDomain (n,m) dom) neqs' = nub (appNNs (n,m) neqs) accs' = nub (appNRNs (n,m) accs) ufs' = nub (appFs (n,m) ufs) boxes' = nub (appNRFs (n,m) boxes) newboxes = boxes' \\ boxes cboxes' = nub (appNRFs (n,m) cboxes) newcboxes = cboxes' \\ cboxes pos' = nub (appNPs (n,m) pos) neg' = nub (appNPs (n,m) neg) fs' = nub (appFs (n,m) fs) newaccs = accs' \\ accs us = [ At m g | g <- ufs' ] bs1 = [ At l g | (k,r,l) <- newaccs, (k',r',g) <- boxes', k == k', r == r' ] bs2 = [ At l g | (k,r,l) <- accs', (k',r',g) <- newboxes, k == k', r == r' ] cs1 = [ At k g | (k,r,l) <- newaccs, (l',r',g) <- cboxes', l == l', r == r' ] cs2 = [ At k g | (k,r,l) <- accs', (l',r',g) <- newcboxes, l == l', r == r' ] newfs = nub (fs' ++ us ++ bs1 ++ bs2 ++ cs1 ++ cs2) in check (Nd i dom' neqs' accs' ufs' boxes' cboxes' pos' neg' newfs) \end{code} The list of pending formulas starts with a negated nominal: check for closure. If the node does not close, add a new inequality $m \NEQ n$ to the inequality list of the node. \begin{code} | ngNom f = if (getNom f) == nom then [] else let k = getNom f m = min k nom n = max k nom neqs' = add (m,n) neqs in [Nd i dom neqs' accs ufs boxes cboxes pos neg fs] \end{code} The list of pending formulas starts with an access formula $@ k \Diamond_i n$. Check whether the access relation $kR_in$ is already present at the node. If not, add it, generate the list $[ @ n \phi \mid A \phi \in U ],$ where $U$ is the list of universal constraints of the node, the list $[ @ n \phi \mid @ k \Ibox{i} \phi \in B ],$ where $B$ is the set of $\Box$ constraints of the node, and the list $[ @ k \phi \mid @ n \Icbox{i} \phi \in C ],$ where $C$ is the set of $\Cbox$ constraints of the node, and append these lists to the list of pending formulas. \begin{code} | isAcc f = let (r,n) = (getRel f, getNom f) accs' = add (nom,r,n) accs dom' = add n dom fs' = if elem (nom,r,n) accs then fs else nub (fs ++ us ++ bs ++ cs) us = [ At n g | g <- ufs ] bs = [ At n g | (m,s,g) <- boxes, m == nom, s == r ] cs = [ At nom g | (m,s,g) <- cboxes, m == n, s == r ] in checkNdNom (Nd i dom' neqs accs' ufs boxes cboxes pos neg fs') \end{code} The list of pending formulas starts with a converse access formula $@ k \Diamond^{\breve{}}_i n$. Check whether the access relation $nR_ik$ is already present at the node. If not, add it, generate the list $[ @ n \phi \mid A \phi \in U ],$ where $U$ is the set of universal constraints of the node, the list $[ @ n \phi \mid @ k \Icbox{i} \phi \in C ],$ where $C$ is the set of $\Box^{\breve{}}$ constraints of the node, and the list $[ @ k \phi \mid @ n \Ibox{i} \phi \in B ],$ where $B$ is the set of $\Box$ constraints of the node, and append these lists to the list of pending formulas. \begin{code} | isCacc f = let (r,n) = (getRel f, getNom f) accs' = add (n,r,nom) accs dom' = add n dom fs' = if elem (n,r,nom) accs then fs else nub (fs ++ us ++ bs ++ cs) us = [ At n g | g <- ufs ] bs = [ At nom g | (m,s,g) <- boxes, m == n, s == r ] cs = [ At n g | (m,s,g) <- cboxes, m == nom, s == r ] in checkNdNom (Nd i dom' neqs accs' ufs boxes cboxes pos neg fs') \end{code} The list of pending formulas starts with a double negation: apply the double negation rule. \begin{code} | dneg f = let [g] = lcomponents nom f fs' = add g fs in [Nd i dom neqs accs ufs boxes cboxes pos neg fs'] \end{code} The list of pending formulas starts with an $\alpha$ formula: add the components $\alpha_i$ to the node. \begin{code} | alpha f = let fs' = nub ((lcomponents nom f) ++ fs) in [Nd i dom neqs accs ufs boxes cboxes pos neg fs'] \end{code} The list of pending formulas starts with a $\beta$ formula: split the node and add a component $\beta_i$ to each new branch. \begin{code} | beta f = [ Nd i dom neqs accs ufs boxes cboxes pos neg (f':fs) | f' <- lcomponents nom f ] \end{code} The list of pending formulas starts with an $A$ formula $@ k \phi$. Add $\{ @ m \phi' \mid m \in D \}$ where $D$ is the domain of the node, to the list of pending formulas, and store $\phi'$ as a universal constraint. \begin{code} | isA f = let newfs = [ At n g | n <- dom, g <- components f ] fs' = nub (fs ++ newfs) [f'] = components f ufs' = nub (f':ufs) in checkNdNom (Nd i dom neqs accs ufs' boxes cboxes pos neg fs') \end{code} The list of pending formulas starts with an $E$ formula $@ k \phi$. Take a fresh nominal $n$, add it to the domain of the node, add $@ n \phi'$ and $\{ @ n \psi \mid \psi \in U \}$ to the list of pending formulas. \begin{code} | isE f = let n = (N i) dom' = add n dom ls = lcomponents n f us = [ At n g | g <- ufs ] fs' = nub (fs ++ ls ++ us) in [Nd (succ i) dom' neqs accs ufs boxes cboxes pos neg fs'] \end{code} The list of pending formulas starts with a $\Ibox{i}$ formula $@k \phi$. Add the list $[ @ m \phi' \mid kR_im \in A ],$ where $A$ is the list of access formulas of the node, to the list of pending formulas, and store the $\Ibox{i}$ formula as a box constraint. Actually, for convenience, we store $(k,i,\phi')$. \begin{code} | box f = let r = getRel f newfs = [ At n g | (m,s,n) <- accs, g <- components f, m == nom, s == r ] fs' = nub (fs ++ newfs) boxes' = nub ([(nom,r,g) | g <- components f] ++ boxes) in checkNdNom (Nd i dom neqs accs ufs boxes' cboxes pos neg fs') \end{code} The list of pending formulas starts with a $\Icbox{i}$ formula $@k \phi$. Add the list $[ @ m \phi' \mid mR_ik \in A ],$ where $A$ is the list of access formulas of the node, to the list of pending formulas, and store the $\Icbox{i}$ formula as a converse box constraint. Actually, for convenience we store $(k,i,\phi')$. \begin{code} | cbox f = let r = getRel f newfs = [ At n g | (n,s,m) <- accs, g <- components f, m == nom, s == r ] fs' = nub (fs ++ newfs) cboxes' = nub ([(nom,r,g) | g <- components f] ++ cboxes) in checkNdNom (Nd i dom neqs accs ufs boxes cboxes' pos neg fs') \end{code} The list of pending formulas starts with a $\Diamond$ formula: use the node index $i$ to generate a fresh nominal constant $n_i$, increment the node index, add $kR_jn_i$ to the access list of the node, and put $@ n_i \phi'$, where $\phi'$ is the component of the $\Diamond$ formula, on the list of pending formulas. Also, generate appropriate formulas for $n_i$ from the universal constraints and from the box constraints on $k$, and append them to the list of pending formulas. \begin{code} | diamond f = let n = (N i) r = getRel f accs' = (nom,r,n):accs dom' = add n dom ls = lcomponents n f us = [ At n g | g <- ufs ] bs = [ At n g | (m,s,g) <- boxes, m == nom, s == r ] fs' = nub (fs ++ ls ++ us ++ bs) in [Nd (succ i) dom' neqs accs' ufs boxes cboxes pos neg fs'] \end{code} The list of pending formulas starts with a $\Cdia$ formula: use the node index $i$ to generate a fresh nominal constant $n_i$, increment the node index, add $n_iR_jk$ to the access list of the node, generate the appropriate formulas for $n_i$ from the converse box constraints of the node, and append them, together with the component of the $\Cdia$ formula, to the list of pending formulas. \begin{code} | cdiamond f = let n = (N i) r = getRel f accs' = (n,r,nom):accs dom' = add n dom ls = lcomponents n f us = [ At n g | g <- ufs ] cs = [ At n g | (m,s,g) <- cboxes, m == nom, s == r ] fs' = nub (fs ++ ls ++ us ++ cs) in [Nd (succ i) dom' neqs accs' ufs boxes cboxes pos neg fs'] \end{code} The list of pending formulas starts with an $@$ formula $@k @n \phi$ (or $@ k \neg @ n \phi$): add $@ n \phi$ (or $@ n \neg \phi$) to the list of pending formulas. \begin{code} | label f = let fs' = add f' fs n = getLabel f [f'] = lcomponents n f in [Nd i dom neqs accs ufs boxes cboxes pos neg fs'] \end{code} The list of pending formulas starts with a $\downarrow$ formula: add its component to the list of pending formulas, after the appropriate substitution. \begin{code} | down f = let x = binder f [g] = components f f' = At nom (appF ((V x),nom) g) fs' = add f' fs in [Nd i dom neqs accs ufs boxes cboxes pos neg fs'] \end{code} These are all the possible cases, so this ends the treatment of a single tableau expansion step. A tableau node is fully expanded (complete) if its list of pending formulas is empty. \begin{code} complete :: Node -> Bool complete (Nd i dom neqs accs ufs boxes cboxes pos neg []) = True complete _ = False \end{code} A tableau is complete if consists of complete nodes: \begin{code} completeT :: Tableau -> Bool completeT = all complete \end{code} Expand a tableau in a fair way by performing an expansion step on a (incomplete) node and moving the result to the end of the node list. \begin{code} fullExpand :: Tableau -> Tableau fullExpand [] = [] fullExpand (node:nodes) = if complete node then node:(fullExpand nodes) else fullExpand (nodes ++ newnodes) where newnodes = step node \end{code} In general, we are not interested in generating all models for a satisfiable formula: one model is enough. This allows for a considerable reduction.\footnote{Note that replacing the two \verb^if then else^ lines by the lines that are commented out permits tracing of the expansion process, for debugging.} \begin{code} expand :: Tableau -> Tableau expand [] = [] expand (node:nodes) = if complete node then [node] else expand (nodes ++ newnodes) -- if complete node then trace (show node ++ "\n\n") [node] -- else trace (show node ++ "\n\n") expand (nodes ++ newnodes) where newnodes = step node \end{code} Tableau development for a given number of steps. Result of \verb^[]^ indicates failure to decide in that many steps. \begin{code} develop :: Int -> Tableau -> [Tableau] develop n t = expandN n t where expandN _ [] = [[]] expandN 0 (nd:nds) = if complete nd then [[nd]] else [] expandN n (nd:nds) = if complete nd then [[nd]] else expandN (n-1) (nds ++ newnodes) where newnodes = step nd \end{code} \section{Cautious Tableau Expansion} Tableau expansion according to the trial and error' versions of the $E$, $\Diamond$ and $\Cdia$ rules is useful for finding minimal models. In cautious tableau expansion we reuse existing nominals, and we should check carefully whether this disturbs our constraints invariant. The following functions take care of this: \begin{code} noAccTo, noAccFrom :: [(Nom,Rel,Nom)] -> Nom -> Rel -> Bool noAccTo accs m r = null [ (k,r,m) | (k,r',m') <- accs, r==r', m==m' ] noAccFrom accs m r = null [ (m,r,k) | (m',r',k) <- accs, r==r', m==m' ] \end{code} Thus, if \verb^noAccTo accs m r^ is true at a node, where \verb^accs^ is the list of access arrows of the node, this means that there is no arrow $x \stackrel{r}{\longrightarrow} m$ at the node. This means in turn that adding a new $r$ arrow that points to $m$ may disturb the box constraint invariant. Similarly, truth of \verb^noAccFrom accs m r^ at a node, for \verb^accs^ is the list of access arrows of the node, indicates that the addition of a new $r$-relation arrow that departs from $m$ may violate the converse box constraint invariant of the node. We are ready now to replace the \verb^step^ function by the following alternative: \begin{code} cautiousStep :: Node -> Tableau \end{code} Cautious step are like ordinary steps, except for the cases where the formula to be decomposed is a $E$, $\Diamond$ and $\Cdia$ formula. If the function is called for a node $N$ with an empty pending formula list, again, there is nothing left to do, and we return $[N]$. \begin{code} cautiousStep (Nd i dom neqs accs ufs boxes cboxes pos neg []) = [Nd i dom neqs accs ufs boxes cboxes pos neg []] \end{code} If the list of pending formulas starts with an $E$ formula, we branch to all the possible ways of letting the existential obligation be fulfilled by an existing nominal, and append the result of doing the extension step that introduces a fresh nominal. Note that no arrows are added, so no box or converse box constraints can be violated. Also, no nominals are added, so no universal constraints can be violated. \begin{code} cautiousStep nd@(Nd i dom neqs accs ufs boxes cboxes pos neg ((At nom f):fs)) | isE f = [ Nd i dom neqs accs ufs boxes cboxes pos neg (nub ((lcomponents n f) ++ fs)) | n <- dom ] ++ (step nd) \end{code} If the list of pending formulas starts with a $\Diamond$ formula, we branch to all the ways of letting an existing nominal discharge the existential obligation, and append the result of the expansion step that introduces a fresh nominal. Now we have to take measures to ensure that the invariant for the box constraints gets restored, if necessary. \begin{code} | diamond f = let r = getRel f in [ Nd i dom neqs (add (nom,r,n) accs) ufs boxes cboxes pos neg (nub ((lcomponents n f) ++ fs ++ [ At n g | (m,s,g) <- boxes, m == nom, s == r, noAccTo accs n r ])) | n <- dom ] ++ (step nd) \end{code} If the list of pending formulas starts with a $\Cdia$ formula, we branch to all the ways of letting an existing individual discharge the existential obligation, and append the result of the expansion step that introduces a fresh nominal. \begin{code} | cdiamond f = let r = getRel f in [ Nd i dom neqs (add (n,r,nom) accs) ufs boxes cboxes pos neg (nub ((lcomponents n f) ++ fs ++ [ At n g | (m,s,g) <- cboxes, m == nom, s == r, noAccFrom accs n r ])) | n <- dom ] ++ (step nd) \end{code} In all other cases, we just perform a regular step: \begin{code} | otherwise = step nd \end{code} \section{Theorem Proving} The function \verb^initTab^ creates an initial tableau for a formula. The initial tableau for $\phi$ just one node, with list of pending formulas $[@ m \phi]$, where $m$ is a fresh nominal. We assume that no nominals of the form \verb^(N i)^ appear in the formula. The node index is set to the index of the first fresh constant nominal, i.e., $1$. \begin{code} initTab :: Form -> Tableau initTab form = [Nd 1 dom [] [] [] [] [] [] [] [At nom form]] where nom = (N 0) dom = nom : (nomsInForm form) \end{code} The function \verb^refuteF^ tries to refute a formula by expanding a tableau for it, and returning \verb^True^ if the tableau closes, \verb^False^ if it remains open. \begin{code} refuteF :: Form -> Bool refuteF form = tableau == [] where tableau = expand (initTab form) \end{code} To prove that a formula is a theorem, feed its negation to the refutation function: \begin{code} thm :: Form -> Bool thm = refuteF . Neg \end{code} Cautious expansion of a tableau:\footnote{Note that replacing the two \verb^if then else^ lines by the lines that are commented out permits tracing of the cautious expansion process, for debugging.} \begin{code} cautiousExpand :: Tableau -> Tableau cautiousExpand [] = [] cautiousExpand (node:nodes) = if complete node then [node] else cautiousExpand (nodes ++ newnodes) -- if complete node then trace (show node ++ "\n\n") [node] -- else trace (show node ++ "\n\n") cautiousExpand (nodes ++ newnodes) where newnodes = cautiousStep node \end{code} Cautious tableau development for a given number of steps. Return of \verb^[]^ indicates failure to decide in that many steps. \begin{code} cdevelop :: Int -> Tableau -> [Tableau] cdevelop n t = cexpandN n t where cexpandN _ [] = [[]] cexpandN 0 (nd:nds) = if complete nd then [[nd]] else [] cexpandN n (nd:nds) = if complete nd then [[nd]] else cexpandN (n-1) (nds ++ newnodes) where newnodes = cautiousStep nd \end{code} \section{Model Generation} \begin{code} extract :: Node -> String extract (Nd i dom _ accs _ _ _ pos neg _) = show (reverse dom) ++ " " ++ concat [ show n ++ "R" ++ show i ++ show m ++ " " | (n,i,m) <- reverse accs ] ++ concat [ "@" ++ show i ++ " p" ++ show p ++ " " | (i,p) <- reverse pos ] ++ concat [ "@" ++ show i ++ "-p" ++ show p ++ " " | (i,p) <- reverse neg ] \end{code} Extract from a (non-empty) tableau: just extract from the first node: \begin{code} extractT :: Tableau -> String extractT (nd:_) = extract nd ++ "\n" \end{code} Report on an expanded tableau, given a string indicating the kind of frame class. As we allow for the possibility that the tableau development was stopped at some treshold value, we have to check whether the tableau is complete. \begin{code} report :: String -> [Tableau] -> IO() report [] [] = putStr ("I don't know whether this is satisfiable\n") report [] [[]] = putStr "not satisfiable\n" report [] [t] = putStr ("satisfiable:\n" ++ extractT t) report frame [] = putStr ("I don't know whether this is satisfiable in \"" ++ frame ++"\" frames\n") report frame [[]] = putStr ("not satisfiable in \"" ++ frame ++ "\" frames\n") report frame [t] = putStr ("satisfiable in a \"" ++ frame ++ "\" frame:\n" ++ extractT t) \end{code} To check a formula for satisfiability, feed it to the proof engine and report on the resulting tableau. \begin{code} sat :: Form -> IO () sat form = report [] [tableau] where tableau = expand (initTab form) \end{code} Check a formula for satisfiability, looking for a minimal model: \begin{code} msat :: Form -> IO () msat form = report [] [tableau] where tableau = cautiousExpand (initTab form) \end{code} \section{Frame Properties} Here is a list of pure formulas (formulas without proposition letters) that define frame properties. In fact, {\em any}\/ pure formula defines a frame condition, and characterizes a class of frames. \begin{center} \begin{tabular}{|l|l|} \hline transitive & $\downarrow x . \Box \Box \Cdia x$ \\ intransitive & $\downarrow x . \Box \Box \Cbox \neg x$ \\ reflexive & $\downarrow x . \Diamond x$ \\ irreflexive & $\downarrow x . \Box \neg x$ \\ symmetric & $\downarrow x . \Box \Cdia x$ \\ asymmetric & $\downarrow x . \Box \Box \neg x$ \\ serial & $\Diamond \top$ \\ euclidean & $\downarrow x . \Box \downarrow y. @ x \Box \Diamond y$ \\ antisymmetric & $\downarrow x . \Box \downarrow y . (x \rightarrow y)$ \\ S4 (refl + trans) & $\downarrow x . (\Diamond x \land \Box \Box \Cdia x)$ \\ S5 (refl + symm + trans) & $\downarrow x . (\Diamond x \land \Box \Diamond x \land \Box \Box \Cdia x)$ \\ \hline \end{tabular} \end{center} To define functions for these, it is convenient to use a function for converting strings to formulas: \begin{code} str2form :: String -> Form str2form = parse . lexer \end{code} Here are the definitions of a number of frame classes that can be extended almost {\em ad libitum}. Many of these are known from modal logic (see \cite{Chellas:ml} or \cite{Popkorn:fsiml} for the abbreviations), but of course the list also contains examples of properties that cannot be defined in standard modal logic. \begin{code} trans = str2form "D x [][]<~>x" k4 = trans intrans = str2form "D x [][][~]-x" refl = str2form "D x <>x" kt = refl irrefl = str2form "D x []-x" symm = str2form "D x []<>x" kb = symm asymm = str2form "D x [][]-x" s4 = str2form "D x (<>x & [][] <~>x)" kt4 = s4 s5 = str2form "D x conj (<>x, []<>x, [][] <~>x)" serial = str2form "<>T" kd = serial euclid = str2form "D x [] D x1 @ x []<>x1" k5 = euclid kdb = str2form "(<>T & D x []<~>x)" kd4 = str2form "(<>T & D x [][]<~>x)" kd5 = str2form "(<>T & D x [] D x1 @ x []<>x1)" k45 = str2form "D x([][]<~>x & [] D x1 @ x []<>x1)" kd45 = str2form "D x conj (<>T, [][]<~>x , [] D x1 @ x []<>x1)" kb4 = str2form "D x ([]<>x & [][] <~>x)" ktb = str2form "D x (<>x & []<>x)" antisymm = str2form "D x [] Dx1 [] (x -> x1)" \end{code} \section{Generic Satisfiability Checking} Distinguish between two modes of satisfiability checking: \verb^Extend^ for extending with a new nominal at each encounter with a diamond, \verb^Try^ for trial and error extension, including checking existing nominals. \begin{code} data Mode = Extend | Try deriving Eq instance Show Mode where show(Extend) = "E" show(Try) = "T" \end{code} If $\psi$ defines a frame property, then any model $\M$ satisfying $A \psi$ will be in the frame class with that property. For suppose that $\M$ does not have the frame property. Then there is a world $w$ with $\M , w \not\models \psi$, hence $\M \not\models A \psi$. Thus, we can build an engine for the frame class of $\psi$ by loading the proof engine with $A \psi$ as a universal constraint. This leads to the following generic satisfiability checker (the first argument gives the mode of satisfiability checking, the second argument lists the formulas defining the frame class under consideration): \begin{code} genSat :: Mode -> [Form] -> Form -> IO() genSat Extend [] form = sat form genSat Try [] form = msat form genSat Extend [prop] form = report str [tableau] where tableau = expand inittab inittab = [Nd 1 dom [] [] [] [] [] [] [] [(At nom form),At nom (A prop)]] nom = (N 0) dom = nom : (nomsInForms [form,prop]) str = show prop genSat Try [prop] form = report str [tableau] where tableau = cautiousExpand inittab inittab = [Nd 1 dom [] [] [] [] [] [] [] [(At nom form),At nom (A prop)]] nom = (N 0) dom = nom : (nomsInForms [form,prop]) str = show prop genSat Extend props form = report str [tableau] where tableau = expand inittab inittab = [Nd 1 dom [] [] [] [] [] [] [] [At nom form, At nom (A (Conj props)) ]] nom = (N 0) dom = nom : (nomsInForms (form:props)) str = show (Conj props) genSat Try props form = report str [tableau] where tableau = cautiousExpand inittab inittab = [Nd 1 dom [] [] [] [] [] [] [] [At nom form, At nom (A (Conj props)) ]] nom = (N 0) dom = nom : (nomsInForms (form:props)) str = show (Conj props) \end{code} \section{Example Formulas} Some examples to play around with: $\Diamond (c \land p) \land \Diamond (c \land p_1) \land \Box( \neg p \lor \neg p_1)$ \begin{code} ex1 = str2form "conj (<> (c & p), <>(c & p1), [] (-p v -p1))" \end{code} $@x \Diamond \Cbox \neg x \lor @ x \Cdia \Box \neg x$ \begin{code} ex2 = str2form "(@x<>[~]-x v @x<~>[]-x)" \end{code} $\Diamond p \land \Diamond \neg p \land \Box(p_1 \rightarrow c) \land \Box p_1$ \begin{code} ex3 = str2form "conj (<>p, <>-p, [](p1 -> c), []p1)" \end{code} $\Diamond (c \land \Diamond c \land \Box \Diamond c)$ \begin{code} ex4 = str2form "<>conj (c, <>c, []<>c)" \end{code} $\Diamond \top \land \Box \Diamond \top \land \Box \downarrow x . \Box \Box \Cdia x$ \begin{code} ex5 = str2form "conj (<>T, []<>T, [] down x [][] <~>x)" \end{code} $\Diamond \top \land \Box \Diamond \top \land \downarrow x . \Box \Box \Cdia x$ Note: this will get the \verb^sat^ function into a loop (why?). The remedy is in the trial and error versions of the $\Diamond$ and $\Cdia$ rules. The \verb^msat^ function finds the minimal model. \begin{code} ex6 = str2form "conj (<>T, []<>T, down x [][] <~>x)" \end{code} The GRID formula from \cite{AreBlaMar:hlcic}: \begin{eqnarray*} @ c \neg \Diamond c & \land & @ c \Diamond \top \\ & \land & @ c \Box \Box \downarrow x . @ c \Diamond x \\ & \land & @ c \Box \downarrow x . \Box \downarrow x_1. @ x \Box \downarrow x_2. @ x \Box \downarrow x_3. (@x_1 x_2 \lor @x_1 x_3 \lor @ x_2 x_3) \\ & \land & @ c \Box \downarrow x . \Box \Box \downarrow x_1. @ x \Box \Box \downarrow x_2. @ x \Box \Box \downarrow x_3. @ x \Box \Box \downarrow x_4. \\ & & \hspace{5em} (@x_1 x_2 \lor @x_1 x_3 \lor @ x_1 x_4 \lor @x_2 x_3 \lor @x_2 x_4 \lor @ x_3 x_4) \end{eqnarray*} \begin{code} grid = str2form ( " conj (@ c -<>c, " ++ " @ c <>T, " ++ " @ c [][] down x @ c <> x, " ++ " @ c [] down x [] down x1 @ x [] down x2 @ x [] down x3 " ++ " disj ( @ x1 x2,@ x1 x3,@ x2 x3 ), " ++ " @ c [] down x [][] down x1 " ++ " @ x [][] down x2 " ++ " @ x [][] down x3 " ++ " @ x [][] down x4 " ++ " disj ( @ x1 x2, @ x1 x3, @ x1 x4, " ++ " @ x2 x3, @ x2 x4, @ x3 x4 ) " ++ " )" ) \end{code} A simple way to input formulas from files: \begin{code} satIO :: IO () satIO = do { putStr "Input file: "; filename <- getLine; fstring <- readFile filename; let { form = str2form fstring; }; putStr ("Formula: " ++ show form ++ "\n"); sat form } \end{code} \begin{code} msatIO :: IO () msatIO = do { putStr "Input file: "; filename <- getLine; fstring <- readFile filename; let { form = str2form fstring; }; putStr ("Formula: " ++ show form ++ "\n"); msat form } \end{code} \label{TabStop} \section{The Main' Module} \label{SectMain} \input{Main} \section{Known Bugs, Future Work} Further testing of the code is (always) necessary. Apart from that, the following are on the agenda: \begin{itemize} \item The parser does not produce useful error messages. Implementing a less primitive version that returns error messages with line numbers is future work. It is probably most useful to make this a joint effort with {\em HyLoRes}. Unfortunately, the {\em HyLoRes}\/ parser does a lot of preprocessing, while we have made it our policy to remain faithful to syntactic form. \item Running of various testbanks of formulas to find bugs and weaknesses. \item Graphical presentation of generated Kripke models, e.g., by incorporation of features from Lex Hendriks' {\em Akka}\/ (see \url{http://turing.wins.uva.nl/~lhendrik/AkkaStart.html}) and Marc Pauly's PDL model editor based on it (see \url{http://www.cwi.nl/~pauly/Applets/ModEd.html}). \item The minimal model search is too clumsy. \item The node compression algorithm from the paper is not yet in the implementation. \item Detailed comparison with {\em HyLoRes} \cite{AreHeg01:hylores}, also written in Haskell. \end{itemize} \paragraph{Acknowledgement} Many thanks to the Dynamo team (Wim Berkelmans, Balder ten Cate, Juan Heguiabehere, Breannd\'an \'O Nuall\'ain) and to Carlos Areces, Patrick Blackburn and Maarten Marx, for useful comments, fruitful discussion and bug chasing help. \bibliographystyle{acm} \bibliography{/home/jve/texmacros/mybibAG,/home/jve/texmacros/mybibHZ} \clearpage \section*{Appendix 1: Lexical Scanning} \input{HylotabLex} \section*{Appendix 2: Source for Happy' Parser Generator } See \url{http://www.haskell.org/happy/} for information about the format. \begin{verbatim} { module HylotabParse where import HylotabLex import Form } %name parse %tokentype { Token } %token at1 { TokenAt1 } at2 { TokenAt2 } prop { TokenProp $$} cst { TokenCst$$ } var { TokenVar $$} true { TokenTrue } false { TokenFalse } neg { TokenNeg } and { TokenAnd } conj { TokenConj } or { TokenOr } disj { TokenDisj } dimp { TokenDimp } impl { TokenImpl } a { TokenA } e { TokenE } box { TokenBox$$ } cbox { TokenCbox $$} dia { TokenDia$$ } cdia { TokenCdia  } bnd { TokenBnd } '(' { TokenOB } ')' { TokenCB } ',' { TokenComma } '.' { TokenDot } %right impl %right dimp %left or %left and %left box cbox dia cdia neg %% Form : cst { Nom (C (read $1)) } | var { Nom (V (read$1)) } | prop { Prop (read $1) } | true { Bool True } | false { Bool False } | a Form { A$2 } | e Form { E $2 } | dia Form { Dia (read$1) $2 } | cdia Form { Cdia (read$1) $2 } | box Form { Box (read$1) $2 } | cbox Form { Cbox (read$1) $2 } | '(' Form dimp Form ')' { Conj [Impl$2 $4,Impl$4 $2] } | '(' Form impl Form ')' { Impl$2 $4 } | neg Form { Neg$2 } | '(' Conjs ')' { Conj (flattenConj (reverse $2)) } | '(' Disjs ')' { Disj (flattenDisj (reverse$2)) } | cst at1 Form { At (C (read $1))$3 } | var at1 Form { At (V (read $1))$3 } | at2 cst Form { At (C (read $2))$3 } | at2 var Form { At (V (read $2))$3 } | bnd var Form { Down (read $2)$3 } | bnd var '.' Form { Down (read $2)$4 } | conj '(' ')' { Bool True } | conj '(' Forms ')' { Conj (reverse $3) } | disj '(' ')' { Bool False } | disj '(' Forms ')' { Disj (reverse$3) } | '(' Form ')' { $2 } Forms : Form { [$1] } | Forms ',' Form { $3 :$1 } Conjs : Form and Form { [$3,$1] } | Conjs and Form { $3:$1 } Disjs : Form or Form { [$3,$1] } | Disjs or Form { $3:$1 } { happyError :: [Token] -> a happyError _ = error "Parse error" } \end{verbatim} \end{document}