tableaux (empty) → 0.1
raw patch · 16 files changed
+1452/−0 lines, 16 filesdep +QuickCheckdep +basedep +cgisetup-changed
Dependencies added: QuickCheck, base, cgi, containers, haskell98, html, mtl, parsec
Files
- INSTALL +12/−0
- LICENSE +27/−0
- README +30/−0
- RELEASE-NOTES +2/−0
- Setup.lhs +8/−0
- src/CSS.hs +53/−0
- src/Examples.hs +51/−0
- src/FOL.hs +106/−0
- src/Main.hs +134/−0
- src/Markup.hs +189/−0
- src/Parser.hs +202/−0
- src/Tableaux.hs +233/−0
- src/Unify.hs +52/−0
- src/Util.hs +24/−0
- src/Zipper.hs +288/−0
- tableaux.cabal +41/−0
+ INSTALL view
@@ -0,0 +1,12 @@++After building with cabal just copy the tableaux.cgi executable+to some cgi-bin directory of your web server (e.g. /var/www/cgi-bin+or ~/public_html/cgi-bin). Make sure you the web server is setup+to execute cgi binaries and that the read-exec permissions are set.++The binary is self-contained so it can be simply be moved if necessary+(no external data files are needed); it also does not write any+files while running.+++Pedro Vasconcelos, 2010
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) Pedro Vasconcelo 2010++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.
+ README view
@@ -0,0 +1,30 @@+Tableaux theorem prover for first order logic+---------------------------------------------++This is a simple interactive theorem prover for first order logic+using the tableaux method. The "tableau" is a tree depicting a proof+where each node is a sentence; linear branches represent conjunctions+while forks represent disjunctions. At each step one introduces+new nodes by "breaking down" a formula into its logical+consequences. To prove a formula F it is sufficient to show that+~F is unsatisfiable, i.e. that all branches of the tableau lead+to contradictions.+ +The prover is implemented in Haskell as a CGI that shows the+current proof tree and highlights one focus node+(initially the whole formula). The interface is consists of:+* navigate the proof tree (point and click)+* expand the current node +* apply resolution to the branch with the current node++Closed branches end in a "false" sentence, i.e. have been shown to +be inconsistent/unsatisfiable. To prove the original theorem one must close+all branches.+++Pedro Vasconcelos <pbv@dcc.fc.up.pt>, 2009.+Tree "zipper" implementation by Krasimir Angelov & Iavor S. Diatchki, 2008.++References: First Order Logic, R. Smullyan, Dover.+On the web: http://en.wikipedia.org/wiki/Method_of_analytic_tableaux+
+ RELEASE-NOTES view
@@ -0,0 +1,2 @@+0.1 - initial release 23/09/2010+
+ Setup.lhs view
@@ -0,0 +1,8 @@+#! /usr/bin/env runhaskell++> module Main (main) where+>+> import Distribution.Simple (defaultMain)+>+> main :: IO ()+> main = defaultMain
+ src/CSS.hs view
@@ -0,0 +1,53 @@+{- + CSS stylesheet for formating tableaux using itemized lists+ images and styles inlined in a Haskell string to simplify installation+ Pedro Vasconcelos, 2010+-}+module CSS (cssText) where++cssText :: String+cssText + = unlines ["ul.tree, ul.tree ul {"+ ,"list-style-type: none;"+ -- background: url(vline.png) repeat-y; + ,"background: url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAEAAAAKAQMAAABPHKYJAAAAA1BMVEWIiIhYZW6zAAAACXBIWXMAAAsTAAALEwEAmpwYAAAAB3RJTUUH1ggGExMZBky19AAAAAtJREFUCNdjYMAEAAAUAAHlhrBKAAAAAElFTkSuQmCC) repeat-y;"+ ,"margin: 0 0 0 10px;"+ ,"padding: 0 0 0 0; }"++ ,"ul.tree li {"+ ,"padding: 0 12px 0 12px;"+ ,"line-height: 1.5;"+ -- background: url(node.png) no-repeat; + ,"background: url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAgAAAAUAQMAAACK1e4oAAAABlBMVEUAAwCIiIgd2JB2AAAAAXRSTlMAQObYZgAAAAlwSFlzAAALEwAACxMBAJqcGAAAAAd0SU1FB9YIBhQIJYVaFGwAAAARSURBVAjXY2hgQIf/GTDFGgDSkwqATqpCHAAAAABJRU5ErkJggg==) no-repeat; }"++ ,"ul.tree li.last {"+ -- background: #fff url(lastnode.png) no-repeat; + ,"background: #fff url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAgAAAAUAQMAAACK1e4oAAAABlBMVEUAAwCIiIgd2JB2AAAAAXRSTlMAQObYZgAAAAlwSFlzAAALEwAACxMBAJqcGAAAAAd0SU1FB9YIBhQIIhs+gc8AAAAQSURBVAjXY2hgQIf/GbAAAKCTBYBUjWvCAAAAAElFTkSuQmCC) no-repeat; }"+ + ,"div.math { font-family: sans-serif; }"+ + ,"span.cursor {"+ ,"border: thin dashed black;"+ ,"background-color: yellow;"+ ,"padding: 1px; }"++ ,"div.conj {"+ -- background: url(vline.png) repeat-y; + ,"background: url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAEAAAAKAQMAAABPHKYJAAAAA1BMVEWIiIhYZW6zAAAACXBIWXMAAAsTAAALEwEAmpwYAAAAB3RJTUUH1ggGExMZBky19AAAAAtJREFUCNdjYMAEAAAUAAHlhrBKAAAAAElFTkSuQmCC) repeat-y;"+ ,"background-position: 10px;"+ ,"padding: 0 0 0 0;"+ ,"margin: 0 0 5px 0; }"++ ,"div.conj p.last { margin: 0 0 0 0; }"++ ,"div.conj p {"+ ,"background: white;"+ ,"margin: 0 0 10px 0; }"++ ,".closed { font-style: oblique; }"++ ,".unused { font-weight: bold; }"++ ,"input#refute { font-family: monospace; }"+ ]+
+ src/Examples.hs view
@@ -0,0 +1,51 @@++module Examples where+import FOL+import Text.Html++infixr -->++(-->) :: Formula -> Formula -> Formula+(-->) = Implies+++examples :: [(String, Formula)]+examples = [ ("Law of excluded middle",+ (p `Or` Not p)+ )+ , ("Contraposition", + ((p-->q)-->(Not q --> Not p)))+ , ("Contradiction",+ p--> (Not p --> q)+ )+ , ("Pierce's law",+ ((p-->q) -->p)-->p+ )+ , ("Distributivity of ∧ over ∨", + (p`Or`(q`And`r)) --> ((p`Or`q)`And`(p`Or`r)))+-- , ("Distributivity of ∨ over ∧", +-- (p`And`(q`Or`r)) --> ((p`And`q)`Or`(p`And`q)))+ , ("Distributivity of ∀ over ⇒",+ Forall "X" (pp "X" --> qq "X") -->+ (Forall "X" (pp "X") --> Forall "X" (qq "X"))+ )+-- , ("Distributivity of ∀ over ∧", +-- (Forall "X" ((pp "X")`And`(qq "X"))) --> +-- (Forall "X" (pp "X") `And`+-- Forall "X" (qq "X"))+-- )+ , ("Moving ∃ across ∀",+ Exist "X" (Forall "Y" (Rel "p" [Var "X", Var "Y"])) -->+ Forall "Y" (Exist "X" (Rel "p" [Var "X", Var "Y"]))+ )+ , ("An example of Skolemization",+ (Forall "X" (Exist "Y" (Rel "p" [Var "X", Var "Y"])))+ --> Exist "Y" (Rel "p" [Fun "a" [], Var "Y"])+ )+ ]+ where p = Rel "p" []+ q = Rel "q" []+ r = Rel "r" []+ pp x = Rel "p" [Var x]+ qq x = Rel "q" [Var x]+
+ src/FOL.hs view
@@ -0,0 +1,106 @@+{- + Abstract syntax for first order logic+ Pedro Vasconcelos, 2009--2010+ pbv@dcc.fc.up.pt+ -}+module FOL where+import List+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Tree+import Zipper hiding (delete)++-- type synonyms for names of variables, +-- functional and relational symbols+type Var = String+type Funsym = String+type Relsym = String++-- first order logic formulas +data Formula = TT+ | FF+ | Rel Relsym [Term]+ | Not Formula + | And Formula Formula+ | Or Formula Formula + | Implies Formula Formula+ | Exist Var Formula+ | Forall Var Formula+ deriving (Eq,Show,Read)++-- instance Show Formula where+-- showsPrec p f = showsFormula p f++-- first order logic terms +data Term = Var Var+ | Fun Funsym [Term]+ deriving (Eq, Show, Read)++-- substitutions: mappings from variables to terms+type Subst = Map Var Term++-- a general class for data types with free variables+class FV a where+ fv :: a -> [Var]+ subst :: Subst -> a -> a++-- instance for terms+instance FV Term where+ fv (Var x) = [x]+ fv (Fun f ts) = concatMap fv ts+ subst s (Var v) = Map.findWithDefault (Var v) v s+ subst s (Fun f ts) = Fun f $ map (subst s) ts++-- instance for formulas+instance FV Formula where+ fv TT = []+ fv FF = []+ fv (Rel r ts) = concatMap fv ts+ fv (Not f) = fv f+ fv (And f1 f2) = fv f1 ++ fv f2+ fv (Or f1 f2) = fv f1 ++ fv f2+ fv (Implies f1 f2) = fv f1 ++ fv f2+ fv (Exist x f) = delete x (nub (fv f))+ fv (Forall x f) = delete x (nub (fv f))+ --+ subst s TT = TT+ subst s FF = FF+ subst s (Rel r ts) = Rel r $ map (subst s) ts+ subst s (Not f) = Not (subst s f)+ subst s (And f1 f2) = And (subst s f1) (subst s f2)+ subst s (Or f1 f2) = Or (subst s f1) (subst s f2)+ subst s (Implies f1 f2) = Implies (subst s f1) (subst s f2)+ subst s (Exist x f) = Exist x (subst s' f)+ where s' = Map.delete x s+ subst s (Forall x f) = Forall x (subst s' f)+ where s' = Map.delete x s+++-- derived instances for parametric types+instance FV a => FV [a] where+ fv ts = concatMap fv ts+ subst s ts = map (subst s) ts++instance (FV a, FV b) => FV (a,b) where+ fv (u,v) = fv u ++ fv v+ subst s (u,v) = (subst s u, subst s v)++instance (FV a, FV b, FV c) => FV (a,b,c) where+ fv (u,v,w) = fv u ++ fv v ++ fv w+ subst s (u,v,w) = (subst s u, subst s v, subst s w)++instance FV a => FV (Maybe a) where+ fv Nothing = []+ fv (Just x) = fv x+ subst s Nothing = Nothing+ subst s (Just x)= Just (subst s x)++instance FV a => FV (Tree a) where+ fv (Node n ts) = fv n ++ concatMap fv ts+ subst s (Node n ts) = Node (subst s n) (map (subst s) ts)++instance FV a => FV (TreeLoc a) where+ fv (Loc t l r ps) = fv t ++ fv l ++ fv r ++ fv ps+ subst s (Loc t l r ps) = Loc (subst s t) (subst s l) (subst s r) (subst s ps)++
+ src/Main.hs view
@@ -0,0 +1,134 @@+{-+ Tableaux theorem prover for first order logic++ Pedro Vasconcelos <pbv@dcc.fc.up.pt>, 2009--2010+-}+module Main where+import Text.Html+import Network.CGI+import FOL+import Tableaux+import Markup+import Examples+import Parser+import Zipper+import Util+import Control.Monad.State+import qualified Data.Map as Map++main :: IO ()+main = runCGI cgi_start++-- CGI entry point +cgi_start = do opstart <- getInput "refute" -- parse a formula to refute+ case opstart of+ Just txt -> cgi_refute (parseFormula txt)+ Nothing -> -- fetch current tableau + do script<-scriptName+ cmds <- getInputWithDefault "cmd" ""+ op1 <- getInput "tableau" + op2 <- getInput "status" + let optf = do t <- op1 + s <- op2+ return (Form script + (read $ unquote t) + (read $ unquote s))+ case optf of+ Just tf -> cgi_tableau tf cmds+ Nothing -> do setHeader "Content-type" "text/html"+ output (renderHtml (greetings script))++cgi_refute (Left msg)+ = do setHeader "Content-type" "text/plain"+ output (show msg)+cgi_refute (Right f)+ = do script<-scriptName + cgi_tableau (Form script tableau initial_status) ""+ where tableau = newTableau (Not f)+++cgi_tableau t cmds + = do setHeader "Content-type" "text/html"+ output (renderHtml (htmlpage << tableau_header t'))+ where t' = foldl perform t cmds++++perform :: Form -> Char -> Form+perform t 'u' = t { form_tableau = cursorUp (form_tableau t) }+perform t 'd' = t { form_tableau = cursorDown (form_tableau t) }+perform t 'l' = t { form_tableau = cursorLeft (form_tableau t) }+perform t 'r' = t { form_tableau = cursorRight (form_tableau t) }+perform t 'x' = let ft = form_tableau t+ st = form_status t+ (ft', st') = runState (expand ft) st+ in t { form_tableau=ft', form_status=st' }++perform t 's' = t { form_tableau=resolve (form_tableau t) }+perform t _ = t+++getInputWithDefault :: MonadCGI m => String -> String -> m String+getInputWithDefault var def = do opt<-getInput var+ return (maybe def id opt)+++tableau_header t+ = [h2 << "Instructions",+ form![action (form_script t), method "POST"] << ordList + [ primHtml "Use <EM>Expand</EM> to split a formula into sub components.",+ primHtml "Move the current focus node by clicking on sub-formulas.",+ primHtml "Use <EM>Resolve</EM> on an <EM>atomic</EM> formula to unify with another of inverted sign in the same branch (thus <EM>closing</EM> the branch).",+ toHtml "The proof is complete when all branches are closed, i.e. end in False.",+ ("To return to the start page, click " +++ submit "bt" "Restart")+ ],+ hr,+ p << math << t,+ hr,+ signature+ ]+ +++-- startup page+-- allows typing in a formula or selecting an example+greetings script + = htmlpage << + [ h1 << "Welcome to the interactive tableaux prover",+ p << [ toHtml "This web page allows constructing proofs of ",+ toHtml "propositional and first-order logic sentences using ",+ toHtml "the method of semantic tableaux. To learn more about tableaux, check the ",+ anchor![href "http://en.wikipedia.org/wiki/Method_of_analytic_tableaux"] << "Wikipedia article."+ ],+ form![action script, method "POST"] << + [ p << "Please type in a formula to prove or choose an example from the list below.",+ p << [inputField "refute"![size "60"], submit "bt" "Start"]+ , p << table << map make_example (zip [1..] examples)+ , hr+ , p << [ toHtml "This theorem prover is written in "+ , anchor![href "http://www.haskell.org"] << "Haskell;"+ , toHtml " the source code package is available in the "+ , anchor![href "http://hackage.haskell.org"] << "HackageDB site."+ ]+ , signature+ ]+ ]+ where+ -- n-th example + make_example (n,(txt,f))+ = tr << [td << input ![name "sel", thetype "radio", + value (show n), onclick cmd],+ td << math << f,+ td![align "right"] << primHtml txt,+ hiddenField id (showFormula f)+ ]+ + where cmd = "copy('" ++ id ++ "')"+ id = "ex" ++ show n+++signature =+ address << [toHtml "Pedro Vasconcelos <pbv@ncc.up.pt>",+ br,+ toHtml "LIACC, University of Porto, PORTUGAL"]+
+ src/Markup.hs view
@@ -0,0 +1,189 @@+{- + HTML pretty-printing for formulas and tableaux ++ Pedro Vasconcelos, 2010.+-}+module Markup where++import FOL+import Tableaux+import Text.Html+import Data.Tree+import Zipper+import Parser+import Util+import CSS+import List(intersperse,span)+++data Form = Form {+ form_script :: String+ , form_tableau :: Tableau+ , form_status :: Status+ } deriving (Eq, Show, Read)+++instance HTML Form where+ toHtml t = form![strAttr "id" "tableau",+ action (form_script t ++ "#focus"), method "POST"] << + [math << (fmap decorate+ (addPaths + (form_tableau t))),+ hiddenField "tableau" (quote (show (form_tableau t))),+ hiddenField "status" (quote (show (form_status t))),+ hiddenField "cmd" ""+ ]+++-- decorate a single tree node+decorate :: (AttrFormula,String) -> Html+decorate (f,p) = markup_path p $ toHtml f++markup_path :: String -> Html -> Html+markup_path [] html+ = thespan <<+ [ thespan![theclass "cursor"] << html+ , spaceHtml+ , button "b1" "Expand" ![onclick "move('x')"]+ , button "b2" "Resolve"![onclick "move('s')"]+ , anchor![name "focus"] << noHtml+ ]+markup_path p html = thespan![onclick ("move('"++p++"')")] << html++++instance HTML AttrFormula where+ toHtml (AttrFormula f open uses)+ | not open = thespan![theclass "closed"] << toHtml f+ | uses>0 = toHtml f+ | otherwise= thespan![theclass "unused"] << toHtml f+++instance HTML Formula where+ toHtml f = htmlFormula 0 f ++-- pretty-print a formula in Html+htmlFormula :: Int -> Formula -> Html+htmlFormula _ TT = toHtml "True"+htmlFormula _ FF = toHtml "False"+htmlFormula _ (Rel r ts) = htmlTerm (Fun r ts)+htmlFormula p (Forall x f)+ = htmlParen (p>10) $ + primHtml "∀" +++ htmlSym x +++ spaceHtml +++ htmlFormula 10 f+htmlFormula p (Exist x f)+ = htmlParen (p>10) $ + primHtml "∃" +++ htmlSym x +++ spaceHtml +++ htmlFormula 10 f+htmlFormula p (Not f)+ = htmlParen (p>10) $ primHtml "¬" +++ htmlFormula 10 f+htmlFormula p (And f1 f2) + = htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "∧" +++ htmlFormula 5 f2+htmlFormula p (Or f1 f2) + = htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "∨" +++ htmlFormula 5 f2+htmlFormula p (Implies f1 f2)+ = htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "⇒" +++ htmlFormula 5 f2+++htmlParen :: Bool -> Html -> Html+htmlParen True h = toHtml "(" +++ h +++ toHtml ")"+htmlParen False h = h+++htmlTerm :: Term -> Html+htmlTerm (Var x) = htmlSym x+htmlTerm (Fun f ts) + | null ts = htmlSym f+ | otherwise = htmlSym f +++ toHtml "(" ++++ concatHtml (intersperse (toHtml ",") (map htmlTerm ts))+ +++ toHtml ")"++htmlSym :: String -> Html+htmlSym "" = noHtml+htmlSym ('_':xs) = sub (htmlSym xs)+htmlSym xs = let (xs',xs'') = span (/='_') xs+ in toHtml xs' +++ htmlSym xs''++++instance HTML a => HTML (Tree a) where+ toHtml (Node x []) = toHtml x+ toHtml t = mkconj (conj t) +++ mkdisj (disj t)+ where conj (Node x [t]) = x : conj t + conj (Node x ts) = [x]+ disj (Node x [t]) = disj t+ disj (Node x ts) = ts+++mkconj :: HTML a => [a] -> Html+mkconj [] = noHtml+mkconj xs + = thediv![theclass "conj"] << (hs ++ [h])+ where hs = map (p.toHtml) (init xs)+ h = p![theclass "last"] << last xs+++mkdisj :: HTML a => [Tree a] -> Html+mkdisj [] = noHtml+mkdisj ts = ulist![theclass "tree"] << (hs ++ [h])+ where hs = map (li.toHtml) (init ts)+ h = li![theclass "last"] << last ts+++instance HTML a => HTML (TreeLoc a) where+ toHtml loc = concatHtml $ toForest $ fmap toHtml loc+++-- miscelaneous Html tags+htmlpage b = [header << [css << cssText, script << jsText],+ body << b]+++script code = Html [HtmlTag "SCRIPT" [strAttr "type" "text/javascript"] code]++css txt = style![thetype "text/css"] << txt++-- stylesheet url = thelink noHtml![rel "stylesheet", thetype "text/css", href url]++math = thediv![theclass "math"] ++-- conj = thediv![theclass "conj"]+++button :: String -> String -> Html+button name value + = input![strAttr "type" "button",+ strAttr "name" name, + strAttr "id" name,+ strAttr "value" value] +++onclick :: String -> HtmlAttr+onclick = strAttr "onclick"++onload :: String -> HtmlAttr+onload = strAttr "onload"++inputField :: String -> Html+inputField name+ = input![strAttr "name" name, strAttr "id" name]+++hiddenField :: String -> String -> Html+hiddenField name value+ = input![strAttr "type" "hidden", strAttr "name" name, + strAttr "id" name, strAttr "value" value]+++-- auxiliary event-handling javascript code+jsText :: String+jsText + = unlines [""+ ,"function move(action)"+ , "{"+ ,"document.getElementById('cmd').value = action;"+ ,"document.getElementById('tableau').submit();"+ ,"}" + ,"function copy(ex)"+ , "{"+ , "document.getElementById('refute').value = document.getElementById(ex).value;"+ , "}"+ ]
+ src/Parser.hs view
@@ -0,0 +1,202 @@+{-+ Parser & pretty-printer for first order logic formulas+ Built using the Parsec Haskell library++ Pedro Vasconcelos, 2009--2010+-}+module Parser where+import FOL+import Text.ParserCombinators.Parsec+import Text.ParserCombinators.Parsec.Char+import Text.ParserCombinators.Parsec.Expr+import qualified Text.ParserCombinators.Parsec.Token as P+import Text.ParserCombinators.Parsec.Language+import Control.Monad+import Char+import List (intersperse)+import Test.QuickCheck++-- setup a tokenizer+lexer :: P.TokenParser ()+lexer = P.makeTokenParser + (emptyDef {reservedNames=["forall", "exist", "true", "false"]})+ ++-- tokens (using Parsec tokenizer)+identifier = P.identifier lexer+reserved = P.reserved lexer+whiteSpace = P.whiteSpace lexer+parens = P.parens lexer+comma = P.comma lexer+natural = P.natural lexer+operator n = string n >> whiteSpace+lexeme = P.lexeme lexer++-- parse formulas (entry function)+parseFormula txt+ = parse (do {f<-connectives; whiteSpace; eof; return f}) "stdin" txt++-- a formula built from connectives+connectives :: Parser Formula+connectives = buildExpressionParser table formula+ where table = [[unary "~" Not],+ [binary "&" And AssocLeft,+ binary "/\\" And AssocLeft],+ [binary "|" Or AssocLeft,+ binary "\\/" Or AssocLeft,+ binary "->" Implies AssocRight]]+ unary name fun + = Prefix (do {operator name; return fun})+ binary name fun assoc + = Infix (do {operator name; return fun}) assoc++formula :: Parser Formula+formula = do { reserved "forall" + ; x<-variable+ ; f<-formula+ ; return (Forall x f)+ }+ <|> do { reserved "exist"+ ; x<-variable+ ; f<-formula+ ; return (Exist x f)+ }+ <|> do { operator "~"; f<-formula; return (Not f) }+ <|> parens connectives+ <|> atomic++-- an atom is either a literal or true/false constant+atomic :: Parser Formula+atomic = do { reserved "true"; return TT }+ <|> do { reserved "false"; return FF }+ <|> do { r<-constant+ ; do { ts<-parens (term`sepBy`comma)+ ; return (Rel r ts) + } <|> + return (Rel r [])+ }+ <?> "atomic formula"++term :: Parser Term+term = do { id<-constant+ ; parens (do { ts<-term`sepBy`comma + ; return (Fun id ts)+ })+ <|> return (Fun id [])+ }+ <|> do { x<-variable; return (Var x) }+ <?> "term"+++constant :: Parser Funsym+constant = lexeme (do { c<-lower+ ; cs<-many alphaNum+ ; return (c:cs)+ }) + <|> do { n<-natural+ ; return (show n) + } + <?> "constant"++variable :: Parser Var+variable = lexeme (do { c<-upper+ ; cs<-many alphaNum+ ; return (c:cs) + }) <?> "variable"++-- formula pretty printer+showFormula f = showsFormula 0 f ""++showsFormula :: Int -> Formula -> ShowS+showsFormula _ TT = ("true"++)+showsFormula _ FF = ("false"++)+showsFormula _ (Rel r ts) = showsTerm (Fun r ts)+showsFormula p (Forall x f)+ = showParen (p>10) $ ("forall "++).(x++).(' ':) .showsFormula 10 f+showsFormula p (Exist x f)+ = showParen (p>10) $ ("exist "++).(x++).(' ':) .showsFormula 10 f+showsFormula p (Not f)+ = showParen (p>10) $ ('~':) . showsFormula 10 f+showsFormula p (And f1 f2) + = showParen (p>=5) $ showsFormula 5 f1 . ("/\\"++) . showsFormula 5 f2+showsFormula p (Or f1 f2) + = showParen (p>=5) $ showsFormula 5 f1 . ("\\/"++) . showsFormula 5 f2+showsFormula p (Implies f1 f2)+ = showParen (p>=5) $ showsFormula 5 f1 . ("->"++) . showsFormula 5 f2++showsTerm :: Term -> ShowS+showsTerm (Var x) = (x++)+showsTerm (Fun c []) = (c++)+showsTerm (Fun f ts) = (f++).('(':).s.(')':)+ where s = foldl (.) id $ intersperse (',':) (map showsTerm ts)++++----------------------------------------------------------------------+-- QuickCheck generators for formulas and terms+----------------------------------------------------------------------+instance Arbitrary Formula where+ arbitrary = sized genFormula+ shrink = shrinkFormula++instance Arbitrary Term where+ arbitrary = sized genTerm+ shrink = shrinkTerm+ +shrinkTerm (Fun f ts) = ts ++ [Fun f ts' | ts'<-shrink ts]+shrinkTerm (Var x) = [Var x]++shrinkFormula (Implies f1 f2) = [f1,f2]+shrinkFormula (And f1 f2) = [f1,f2]+shrinkFormula (Or f1 f2) = [f1,f2]+shrinkFormula (Not f) = [f]+shrinkFormula (Exist x f)= [f]+shrinkFormula (Forall x f) = [f]+shrinkFormula (Rel r ts) = [Rel r ts' | ts'<-shrink ts]+++-- a sized generator for formulas+genFormula :: Int -> Gen Formula+genFormula 0 = elements [TT, FF]+genFormula n | n>0 = frequency [(1, arity 1), (1, arity 2),+ (2, liftM2 And f' f'),+ (2, liftM2 Or f' f'),+ (2, liftM2 Implies f' f'),+ (2, liftM2 Forall variables f''),+ (2, liftM2 Exist variables f'')+ ]+ where+ f' = genFormula (n`div`2)+ f'' = genFormula (n-1)+ arity k = do r<-relsyms+ ts<-sequence [genTerm (n`div`k -1) | _<-[1..k]]+ return (Rel r ts)+ relsyms = elements ["p", "q", "r", "s"]+ variables = elements ["X", "Y", "Z"]+++-- a sized generator for terms+genTerm :: Int -> Gen Term+genTerm n | n<=0 = frequency [(1, liftM (\f -> Fun f []) constants), + (2, liftM Var variables)]+ | otherwise = oneof [arity 1, arity 2]+ where+ arity k = do f<- funsyms+ ts <- sequence [genTerm (n`div`k - 1) | _<-[1..k]]+ return (Fun f ts)+ funsyms = elements ["f", "g", "h"] + constants = elements ["a", "b", "c", "e"]+ variables = elements ["X", "Y", "Z"]+++------------------------------------------------------------------+-- Quickcheck properties follow +------------------------------------------------------------------++-- relation between parsing & pretty-printting+-- parseFromula is the left-inverse of showFormula+prop_parseRoundtrip f = case parseFormula (showFormula f) of+ Left err -> False+ Right f' -> f==f'++
+ src/Tableaux.hs view
@@ -0,0 +1,233 @@+{-+ Theorem prover using the Tableaux method++ Pedro Vasconcelos, 2009-2010+ pbv@dcc.fc.up.pt+-}+module Tableaux where++import FOL+import Unify +import qualified Data.Map as Map+import Maybe ++{- + Data.Tree from Haskell's standard library+ Data.Tree.Zipper is based on the rosezipper package+ A "zipper" is a purely-functional idiom for extending an+ inductive type with a single "hole" (i.e. the active node)+ -}+import Data.Tree+import Zipper ++import Control.Monad+import Control.Monad.State+++-- a tableau is a tree zipper+-- of formula, attributes pairs+type Tableau = TreeLoc AttrFormula++-- a formula with atributes+data AttrFormula = + AttrFormula { formula :: Formula+ , is_open :: !Bool -- True if in an open branch, False if closed+ , use_count :: !Int -- number of times used+ } + deriving (Eq,Show,Read)++-- allow substitutions on atributed formulas +instance FV AttrFormula where+ fv af = fv (formula af)+ subst s af = af { formula = subst s (formula af) }+++-- add atributes to a formula+attr :: Formula -> AttrFormula+attr f = AttrFormula f (f/=FF) 0+++-- make an initial tableau with a single formula+newTableau :: Formula -> Tableau+newTableau f = fromTree (Node (attr f) [])++++-- a state monad for proofs+-- (most general unifier, new var counter, new skolem counter)+type Proof a = State Status a++data Status = Status { vars :: !Int -- variable counter+ , skolems :: !Int -- Skolem function counter+ }+ deriving (Eq,Show,Read)++initial_status :: Status+initial_status = Status { vars=0, skolems=0 } ++-- generate a new variable+newVar :: Proof Var+newVar = do n<-gets vars+ modify (\s -> s { vars=n+1 })+ return ("X_"++show n)++-- generate a new skolem term+newSkolem :: [Var] -> Proof Term+newSkolem vs = do k<-gets skolems+ modify (\s -> s { skolems=k+1 })+ return (Fun ("c_"++show k) (map Var vs))++-- count one extra step+-- incrStep :: Proof ()+-- incrStep = modify (\s -> s{ steps=1+steps s})+++-- perform tableau expansion on the current node+expand :: Tableau -> Proof Tableau+expand loc + = do disj <- expandFormula f+ return (if disj /= [[f]] then+ modifyTree (append_open (attrs disj) . incr_uses) loc+ else+ loc)+ where f = formula (rootLabel (tree loc))+ attrs = map (map attr) -- add default atributes+++incr_uses :: Tree AttrFormula -> Tree AttrFormula+incr_uses (Node x ts) = Node x' ts+ where x' = x { use_count = 1+use_count x }+++-- append at the end of open branches +append_open :: [[AttrFormula]] -> Tree AttrFormula -> Tree AttrFormula+append_open disj t + | not (is_open (rootLabel t)) = t+append_open disj (Node f ts) + | null ts = Node f (fromDisj disj)+ | otherwise = Node f (map (append_open disj) ts)+ +fromDisj :: [[a]] -> Forest a+fromDisj [[p],[q]] = [Node p [], Node q []]+fromDisj [[p, q]] = [Node p [Node q []]]+fromDisj [[p]] = [Node p []]+fromDisj [] = []++++-- auxiliary function to expand a formula+expandFormula :: Formula -> Proof [[Formula]]++-- conjuction and disjunction+expandFormula (And p q) = return [[p,q]]+expandFormula (Or p q) = return [[p],[q]]++-- implication+expandFormula (Implies p q) = return [[Not p],[q]]++-- quantification+expandFormula (Forall x p) + = do x'<-newVar+ let s = Map.singleton x (Var x')+ return [[subst s p]]+ +expandFormula f@(Exist x p) + = do t<-newSkolem (fv f)+ let s = Map.singleton x t+ return [[subst s p]]++-- negated forms+expandFormula (Not TT) = return [[FF]]+expandFormula (Not FF) = return [[TT]]++expandFormula (Not (Not p)) = return [[p]]++expandFormula (Not (And p q)) + = return [[Not p], [Not q]]++expandFormula (Not (Or p q)) + = return [[Not p, Not q]]++expandFormula (Not (Implies p q)) + = return [[p, Not q]]++expandFormula (Not (Forall x p)) + = return [[Exist x (Not p)]]++expandFormula (Not (Exist x p)) + = return [[Forall x (Not p)]]++-- default rule: no expansion +expandFormula f = return [[f]]++++-- use resolution to attempt to close the current branch+resolve :: Tableau -> Tableau+resolve loc + = case msum [resolve_atom f f' | + f'<-map formula (ancestorLabels loc)] of+ Nothing -> loc+ Just s -> update_closed $ + modifyTree (incr_uses . close) (subst s loc)+ where f = formula (rootLabel (tree loc))+ close (Node x _) = Node (x{is_open=False}) [Node (attr FF) []]+++-- resolution of two atomic formulas+resolve_atom :: Formula -> Formula -> Maybe Subst+resolve_atom (Rel r ts) (Not (Rel r' ts'))+ | r==r' && length ts==length ts' = unifyEqs Map.empty (zip ts ts')+resolve_atom f@(Not (Rel r ts)) f'@(Rel r' ts') = resolve_atom f' f+resolve_atom _ _ = Nothing++++-- check whether a formula is a positive/negative literal+atomic :: Formula -> Bool+atomic (Rel r ts) = True+atomic (Not (Rel r ts)) = True+atomic _ = False+++-- list the ancestors of a tree location+ancestorLabels :: TreeLoc a -> [a]+ancestorLabels = map (rootLabel.tree) . ancestors ++ancestors :: TreeLoc a -> [TreeLoc a]+ancestors loc = loc : maybe [] ancestors (parent loc)++++-- move the cursor (leaving the position unchanged when not applicable)+cursorLeft, cursorRight, cursorUp, cursorDown :: TreeLoc a -> TreeLoc a+cursorLeft loc = maybe loc id (left loc)+cursorRight loc = maybe loc id (right loc)+cursorUp loc = maybe loc id (parent loc)+cursorDown loc = maybe loc id (firstChild loc)+++-- collect all leaves of a tree+leaves :: Tree a -> [a]+leaves (Node x []) = [x]+leaves (Node _ ts) = concatMap leaves ts++++-- update open/closed attributes+update_closed :: Tableau -> Tableau+update_closed loc+ | is_open_branch loc = loc+ | otherwise + = let loc' = close_node loc+ in maybe loc' update_closed (parent loc')++close_node :: Tableau -> Tableau+close_node = modifyTree (\(Node f ts) -> Node (f{is_open=False}) ts) +++-- check if the current node is an open branch+is_open_branch :: Tableau -> Bool+is_open_branch loc = or (map (is_open . rootLabel) (subForest (tree loc)))++
+ src/Unify.hs view
@@ -0,0 +1,52 @@+{- + Robinson's unification algorithm for first order terms+ Pedro Vasconcelos, 2009+ pbv@dcc.fc.up.pt+ -}+module Unify(unifyEqs) where++import FOL +import qualified Data.Map as Map++-- unification algorithm+-- the inputs are the current unifier substitution+-- and a list of pairs of terms to unify (i.e. equations)+unifyEqs :: Subst -> [(Term,Term)] -> Maybe Subst+unifyEqs s [] = return s +unifyEqs s ((t,t'):eqs) = unifyEqs' s (subst s t) (subst s t') eqs++-- auxiliary function+-- pre-condition: the unifying substitution has already been applyed+unifyEqs' :: Subst -> Term -> Term -> [(Term,Term)] -> Maybe Subst+unifyEqs' s (Var x) (Var y) eqs + | x==y = unifyEqs s eqs+ | x<y = unifyEqs (s `extend` (y,Var x)) eqs+ | otherwise = unifyEqs (s `extend` (x,Var y)) eqs+unifyEqs' s (Var x) t eqs + | x`notElem`fv t = unifyEqs (s `extend` (x,t)) eqs+ | otherwise = fail "occur check failed"++unifyEqs' s t (Var x) eqs = unifyEqs' s (Var x) t eqs++unifyEqs' s (Fun f ts) (Fun f' ts') eqs+ | f==f' && length ts==length ts' = unifyEqs s (zip ts ts' ++ eqs)+ | otherwise = fail "unification failed" ++-- note that "fail" for the Maybe monad is Nothing+++-- extend a substitution+extend :: Subst -> (Var,Term) -> Subst+s `extend` (v,t) = Map.insert v t s ++-- compose two substitutions+-- note that Map.union is left-biased+-- compose :: Subst -> Subst -> Subst+-- compose s2 s1 = Map.map (subst s2) s1 `Map.union` s2+++-- restrict a substitution+-- remove bindings for a list of variables+-- restrict :: Subst -> [Var] -> Subst+-- s `restrict` vs = foldr Map.delete s vs+
+ src/Util.hs view
@@ -0,0 +1,24 @@++module Util where+import Char+import Test.QuickCheck+++quote :: String -> String+quote = concatMap qchar + where qchar x | isUnquoted x = [x]+ | otherwise = '#':shows (ord x) ";"++isUnquoted :: Char -> Bool+isUnquoted x = x/='\"' && x/='\'' && x/='#'+++unquote :: String -> String+unquote str+ | null str''= str+ | otherwise = str' ++ chr code : unquote str'''+ where (str',str'') = break (=='#') str+ (code,';':str'''):_ = reads (tail str'')+++prop_roundtrip xs = collect (length xs) $ unquote (quote xs) == xs
+ src/Zipper.hs view
@@ -0,0 +1,288 @@+--+-- Copyright (c) Krasimir Angelov 2008.+-- Copyright (c) Iavor S. Diatchki 2008.+--+-- Generic zipper implementation for Data.Tree+--+--++module Zipper+ ( TreeLoc(..)++ -- * Conversions+ , fromTree+ , fromForest+ , toForest+ , toTree++ -- * Moving around+ , parent+ , root+ , getChild+ , findChild+ , firstChild+ , lastChild+ , left+ , right++ -- * Node classification+ , isRoot+ , isFirst+ , isLast+ , isLeaf+ , isChild+ , hasChildren++ -- * Tree-specific mutation+ , insertLeft+ , insertRight+ , insertDownFirst+ , insertDownLast+ , insertDownAt+ , delete++ -- * Working with the current tree+ , setTree+ , modifyTree+ , modifyLabel+ , setLabel+ , getLabel++ -- * Add path labels for navigation+ , addPaths+ ) where++import Data.Tree++-- | A position within a 'Tree'.+data TreeLoc a = Loc+ { tree :: Tree a -- ^ The currently selected tree.+ , lefts :: Forest a -- ^ Siblings on the left, closest first.+ , rights :: Forest a -- ^ Siblings on the right, closest first.+ , parents :: [(Forest a, a, Forest a)]+ -- ^ The contexts of the parents for this location.+ } deriving (Read,Show,Eq)++-- allow mapping of tree zippers+instance Functor TreeLoc where+ fmap f (Loc t ls rs ps) = Loc t' ls' rs' ps'+ where t' = fmap f t+ ls' = map (fmap f) ls+ rs' = map (fmap f) rs+ ps' = [(map (fmap f) l, f x, map (fmap f) r) | (l,x,r)<-ps]++++-- Moving around ---------------------------------------------------------------++-- | The parent of the given location.+parent :: TreeLoc a -> Maybe (TreeLoc a)+parent loc =+ case parents loc of+ (pls,v,prs) : ps -> Just+ Loc { tree = Node v (combChildren (lefts loc) (tree loc) (rights loc))+ , lefts = pls, rights = prs, parents = ps+ }+ [] -> Nothing+++-- | The top-most parent of the given location.+root :: TreeLoc a -> TreeLoc a+root loc = maybe loc root (parent loc)+++-- | The left sibling of the given location.+left :: TreeLoc a -> Maybe (TreeLoc a)+left loc =+ case lefts loc of+ t : ts -> Just loc { tree = t, lefts = ts, rights = tree loc : rights loc }+ [] -> Nothing++-- | The right sibling of the given location.+right :: TreeLoc a -> Maybe (TreeLoc a)+right loc =+ case rights loc of+ t : ts -> Just loc { tree = t, lefts = tree loc : lefts loc, rights = ts }+ [] -> Nothing+++-- | The first child of the given location.+firstChild :: TreeLoc a -> Maybe (TreeLoc a)+firstChild loc =+ case subForest (tree loc) of+ t : ts -> Just+ Loc { tree = t, lefts = [], rights = ts , parents = downParents loc }+ [] -> Nothing++-- | The last child of the given location.+lastChild :: TreeLoc a -> Maybe (TreeLoc a)+lastChild loc =+ case reverse (subForest (tree loc)) of+ t : ts -> Just+ Loc { tree = t, lefts = ts, rights = [], parents = downParents loc }+ [] -> Nothing++-- | The child with the given index (starting from 0).+getChild :: Int -> TreeLoc a -> Maybe (TreeLoc a)+getChild n loc =+ do (t:ls,rs) <- splitChildren [] (subForest (tree loc)) n+ return Loc { tree = t, lefts = ls, rights = rs, parents = downParents loc }++-- | The first child that satisfies a predicate.+findChild :: (Tree a -> Bool) -> TreeLoc a -> Maybe (TreeLoc a)+findChild p loc =+ do (ls,t,rs) <- split [] (subForest (tree loc))+ return Loc { tree = t, lefts = ls, rights = rs, parents = downParents loc }++ where split acc (x:xs) | p x = Just (acc,x,xs)+ split acc (x:xs) = split (x:acc) xs+ split _ [] = Nothing++-- private: computes the parent for "down" operations.+downParents :: TreeLoc a -> [(Forest a, a, Forest a)]+downParents loc = (lefts loc, rootLabel (tree loc), rights loc) : parents loc++++-- Conversions -----------------------------------------------------------------++-- | A location corresponding to the root of the given tree.+fromTree :: Tree a -> TreeLoc a+fromTree t = Loc { tree = t, lefts = [], rights = [], parents = [] }++-- | The location of the first tree in a forest.+fromForest :: Forest a -> Maybe (TreeLoc a)+fromForest (t:ts) = Just Loc { tree = t, lefts = [], rights = ts, parents = [] }+fromForest [] = Nothing++-- | Computes the tree containing this location.+toTree :: TreeLoc a -> Tree a+toTree loc = tree (root loc)++-- | Computes the forest containing this location.+toForest :: TreeLoc a -> Forest a+toForest loc = let r = root loc in combChildren (lefts r) (tree r) (rights r)+++-- Queries ---------------------------------------------------------------------++-- | Are we at the top of the tree?+isRoot :: TreeLoc a -> Bool+isRoot loc = null (parents loc)++-- | Are we at the left end of the the tree?+isFirst :: TreeLoc a -> Bool+isFirst loc = null (lefts loc)++-- | Are we at the right end of the tree?+isLast :: TreeLoc a -> Bool+isLast loc = null (rights loc)++-- | Are we at the bottom of the tree?+isLeaf :: TreeLoc a -> Bool+isLeaf loc = null (subForest (tree loc))++-- | Do we have a parent?+isChild :: TreeLoc a -> Bool+isChild loc = not (isRoot loc)++-- | Do we have children?+hasChildren :: TreeLoc a -> Bool+hasChildren loc = not (isLeaf loc)+++-- The current tree -----------------------------------------------------------+++-- | Change the current tree.+setTree :: Tree a -> TreeLoc a -> TreeLoc a+setTree t loc = loc { tree = t }++-- | Modify the current tree.+modifyTree :: (Tree a -> Tree a) -> TreeLoc a -> TreeLoc a+modifyTree f loc = setTree (f (tree loc)) loc++-- | Modify the label at the current node.+modifyLabel :: (a -> a) -> TreeLoc a -> TreeLoc a+modifyLabel f loc = setLabel (f (getLabel loc)) loc++-- | Change the label at the current node.+setLabel :: a -> TreeLoc a -> TreeLoc a+setLabel v loc = modifyTree (\t -> t { rootLabel = v }) loc++-- Get the current label.+getLabel :: TreeLoc a -> a+getLabel loc = rootLabel (tree loc)+++--------------------------------------------------------------------------------++-- | Insert a tree to the left of the current position.+-- The new tree becomes the current tree.+insertLeft :: Tree a -> TreeLoc a -> TreeLoc a+insertLeft t loc = loc { tree = t, rights = tree loc : rights loc }++-- | Insert a tree to the right of the current position.+-- The new tree becomes the current tree.+insertRight :: Tree a -> TreeLoc a -> TreeLoc a+insertRight t loc = loc { tree = t, lefts = tree loc : lefts loc }++insertDownFirst :: Tree a -> TreeLoc a -> TreeLoc a+insertDownFirst t loc =+ loc { tree = t, lefts = [], rights = subForest (tree loc)+ , parents = downParents loc }++insertDownLast :: Tree a -> TreeLoc a -> TreeLoc a+insertDownLast t loc =+ loc { tree = t, lefts = reverse (subForest (tree loc)), rights = []+ , parents = downParents loc }++insertDownAt :: Int -> Tree a -> TreeLoc a -> Maybe (TreeLoc a)+insertDownAt n t loc =+ do (ls,rs) <- splitChildren [] (subForest (tree loc)) n+ return loc { tree = t, lefts = ls, rights = rs, parents = downParents loc }++-- | Delete the current node. The new position is:+-- * the right sibling, or if none+-- * the left sibling, or if none+-- * the parent.+delete :: TreeLoc a -> Maybe (TreeLoc a)+delete loc =+ case rights loc of+ t : ts -> Just loc { tree = t, rights = ts }+ _ -> case lefts loc of+ t : ts -> Just loc { tree = t, lefts = ts }+ _ -> do loc1 <- parent loc+ return $ modifyTree (\t -> t { subForest = [] }) loc1+++splitChildren :: [a] -> [a] -> Int -> Maybe ([a],[a])+splitChildren acc xs 0 = Just (acc,xs)+splitChildren acc (x:xs) n = splitChildren (x:acc) xs $! n-1+splitChildren _ _ _ = Nothing+++combChildren ls t rs = foldl (flip (:)) (t:rs) ls+++-- * Add path labels to a zipper ++addPaths :: TreeLoc a -> TreeLoc (a,String)+addPaths loc = fmap (\(x,p) -> (x,reverse p)) $+ Loc { tree = addPaths' "" (tree loc)+ , lefts = [addPaths' p t | (t,p)<-zip (lefts loc) (lpaths "")]+ , rights = [addPaths' p t | (t,p)<-zip (rights loc) (rpaths "")]+ , parents = [([addPaths' p' t| (t,p')<-zip ls (lpaths p)],+ (x,p), + [addPaths' p' t | (t,p')<-zip rs (rpaths p)])+ | ((ls,x,rs),p)<-zip (parents loc) upaths]+ }+ where lpaths p = tail $ iterate ('l':) p+ rpaths p = tail $ iterate ('r':) p+ upaths = iterate ('u':) "u"+ ++addPaths' :: String -> Tree a -> Tree (a,String)+addPaths' path (Node x ts) + = Node (x,path) [addPaths' p t | (t,p)<-zip ts paths]+ where paths = iterate ('r':) ('d':path)
+ tableaux.cabal view
@@ -0,0 +1,41 @@+name: tableaux+version: 0.1++category: Theorem Provers++synopsis: An interactive theorem prover based on semantic tableaux++description:+ This is a simple web-based interactive theorem prover + using semantic tableaux for propositional and first-order logic + (cf. "First-Order Logic", Raymond Smullyan, Dover).+ It allows step-by-step construction of proofs and runs on any+ web server supporting the CGI interface.+ ++author: Pedro Vasconcelos <pbv@ncc.up.pt>+maintainer: Pedro Vasconcelos <pbv@ncc.up.pt>++license: BSD3+license-file: LICENSE++build-type: Simple+cabal-version: >= 1.6++extra-source-files:+ README INSTALL RELEASE-NOTES ++executable tableaux.cgi+ hs-source-dirs: src+ main-is: Main.hs+ other-modules: FOL Unify Tableaux Markup CSS Parser Zipper Examples Util + build-depends:+ base >= 4 && < 5,+ haskell98,+ containers,+ mtl >= 1.1,+ html >= 1.0,+ parsec >= 2.1 && <3,+ cgi >= 3001.1,+ QuickCheck >= 2.1+