diff --git a/INSTALL b/INSTALL new file mode 100644 --- /dev/null +++ b/INSTALL @@ -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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -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 , 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 + diff --git a/RELEASE-NOTES b/RELEASE-NOTES new file mode 100644 --- /dev/null +++ b/RELEASE-NOTES @@ -0,0 +1,2 @@ +0.1 - initial release 23/09/2010 + diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,8 @@ +#! /usr/bin/env runhaskell + +> module Main (main) where +> +> import Distribution.Simple (defaultMain) +> +> main :: IO () +> main = defaultMain diff --git a/src/CSS.hs b/src/CSS.hs new file mode 100644 --- /dev/null +++ b/src/CSS.hs @@ -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; }" + ] + diff --git a/src/Examples.hs b/src/Examples.hs new file mode 100644 --- /dev/null +++ b/src/Examples.hs @@ -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] + diff --git a/src/FOL.hs b/src/FOL.hs new file mode 100644 --- /dev/null +++ b/src/FOL.hs @@ -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) + + diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,134 @@ +{- + Tableaux theorem prover for first order logic + + Pedro Vasconcelos , 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 Expand to split a formula into sub components.", + primHtml "Move the current focus node by clicking on sub-formulas.", + primHtml "Use Resolve on an atomic formula to unify with another of inverted sign in the same branch (thus closing 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 ", + br, + toHtml "LIACC, University of Porto, PORTUGAL"] + diff --git a/src/Markup.hs b/src/Markup.hs new file mode 100644 --- /dev/null +++ b/src/Markup.hs @@ -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;" + , "}" + ] diff --git a/src/Parser.hs b/src/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Parser.hs @@ -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' + + diff --git a/src/Tableaux.hs b/src/Tableaux.hs new file mode 100644 --- /dev/null +++ b/src/Tableaux.hs @@ -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))) + + diff --git a/src/Unify.hs b/src/Unify.hs new file mode 100644 --- /dev/null +++ b/src/Unify.hs @@ -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 (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 + diff --git a/src/Util.hs b/src/Util.hs new file mode 100644 --- /dev/null +++ b/src/Util.hs @@ -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 diff --git a/src/Zipper.hs b/src/Zipper.hs new file mode 100644 --- /dev/null +++ b/src/Zipper.hs @@ -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) diff --git a/tableaux.cabal b/tableaux.cabal new file mode 100644 --- /dev/null +++ b/tableaux.cabal @@ -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 +maintainer: Pedro Vasconcelos + +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 +