diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Cameron Brandon White
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Cameron Brandon White nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"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 COPYRIGHT
+OWNER 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.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,63 @@
+HsSymMath
+=========
+
+Interactive mathematical languages written in haskell
+
+## Logic.hs ##
+
+Formal logic parser 
+
+### Command line ###
+
+Currently the command line will take a logical expression as an argument and print out its corresponding truth table.
+
+```
+$ ./Logic
+Enter Command
+> TruthTable: a&b+c->~a&b
+'a'   'b'   'c'   | (((a&b)+c)->(~a&b))
+True  True  True  | False
+True  True  False | False
+True  False True  | False
+True  False False | True 
+False True  True  | True 
+False True  False | True 
+False False True  | False
+False False False | True 
+
+Enter Command
+> ToNand: a&b->c 
+(((((a|b)|(a|b))|((a|b)|(a|b)))|(((a|b)|(a|b))|((a|b)|(a|b))))|(c|c))
+
+Enter Command
+> ToNor: a&b->c
+(((((a/a)/(b/b))/((a/a)/(b/b)))/c)/((((a/a)/(b/b))/((a/a)/(b/b)))/c))
+```
+
+### Code ###
+
+```haskell
+> And (Atom 'a') (Not (Atom 'b'))
+(a&~b)
+
+> truthTable $ And (Atom 'a') (Not (Atom 'b'))
+'a'   'b'   | (a&~b)
+True  True  | False
+True  False | True 
+False True  | False
+False False | False
+
+> toNand $ And (Atom 'a') (Not (Atom 'b'))
+((a|(b|b))|(a|(b|b)))
+
+> toNor $ And (Atom 'a') (Not (Atom 'b'))
+((a/a)/((b/b)/(b/b)))
+
+> let exp = And (Atom 'a') (Not (Atom 'b'))
+> exp == toNand exp
+True
+> exp == toNor exp
+True
+> exp == toNor (toNand exp)
+True
+```
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/WeberLogic.cabal b/WeberLogic.cabal
new file mode 100644
--- /dev/null
+++ b/WeberLogic.cabal
@@ -0,0 +1,33 @@
+-- Initial WeberLogic.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                WeberLogic
+version:             0.1.0.0
+synopsis:            Logic interpreter
+description:         Logic interpreter
+homepage:            https://github.com/cameronbwhite/WeberLogic
+license:             BSD3
+license-file:        LICENSE
+author:              Cameron Brandon White
+maintainer:          cameronbwhite90@gmail.com
+-- copyright:           
+category:            Math
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     WeberLogic.Actions, WeberLogic.Parser
+  -- other-modules:       
+  -- other-extensions:    
+  build-depends:       base >=4.6 && <4.7, parsec >=3.1 && <3.2
+  -- hs-source-dirs:      
+  default-language:    Haskell2010
+
+executable WeberLogic
+  main-is:             WeberLogic.lhs
+  -- other-modules:       
+  -- other-extensions:    
+  build-depends:       base >=4.6 && <4.7, parsec >=3.1 && <3.2
+  -- hs-source-dirs:      
+  default-language:    Haskell2010
diff --git a/WeberLogic.lhs b/WeberLogic.lhs
new file mode 100644
--- /dev/null
+++ b/WeberLogic.lhs
@@ -0,0 +1,65 @@
+> module WeberLogic where
+
+> import System.Environment
+> import System.IO (hFlush, stdout)
+> import Text.Parsec (parse)
+
+> import WeberLogic.Parser
+> import WeberLogic.Actions
+
+> data Command = TruthTable LogicExp
+>             | TruthTree [LogicExp]
+>             | IsArgConsistent [LogicExp]
+>             | ToNand LogicExp
+>             | ToNor LogicExp
+>             | Error String
+
+> main :: IO()
+> main = do
+>   args <- getArgs
+>   reader
+
+> reader :: IO ()
+> reader = do
+>   putStrLn "Enter Command"
+>   putStr "> "
+>   hFlush stdout
+>   line <- getLine                              
+>   runCommand $ readCommand line
+>   reader
+
+> readCommand :: String -> Command
+> readCommand input = case words input of 
+>   ("truthTable:":arguments) -> 
+>       case parse parseExp "truthtable" $ unwords arguments of 
+>               Right val -> TruthTable val
+>               Left val -> Error $ show val
+>   ("truthTree:":arguments) ->
+>       case parse parseArg "truthTree" $ unwords arguments of 
+>               Right val -> TruthTree val
+>               Left val -> Error $ show val
+>   ("toNand:":arguments) ->
+>       case parse parseExp "toNand" $ unwords arguments of 
+>               Right val -> ToNand val
+>               Left val -> Error $ show val
+>   ("toNor:":arguments) ->
+>       case parse parseExp "toNor" $ unwords arguments of 
+>               Right val -> ToNor val
+>               Left val -> Error $ show val
+>   ("isArgConsistent:":arguments) ->
+>       case parse parseArg "isArgConsistent" $ unwords arguments of 
+>               Right val -> IsArgConsistent val
+>               Left val -> Error $ show val
+>   _ -> Error input
+
+> runCommand :: Command -> IO()
+> runCommand cmd = 
+>   case cmd of
+>     TruthTable exp -> mapM_ putStrLn $ truthTableStrs exp
+>     TruthTree exps -> truthTree exps'
+>       where exps' = (take (length exps - 1) exps) ++ [Not (last exps)]
+>     IsArgConsistent exps -> putStrLn $ show $ not $ isConsistent exps'
+>       where exps' = (take (length exps - 1) exps) ++ [Not (last exps)]
+>     ToNand exp     -> putStrLn $ show $ toNand exp
+>     ToNor exp      -> putStrLn $ show $ toNor exp
+>     Error err      -> putStrLn err
diff --git a/WeberLogic/Actions.lhs b/WeberLogic/Actions.lhs
new file mode 100644
--- /dev/null
+++ b/WeberLogic/Actions.lhs
@@ -0,0 +1,269 @@
+> module WeberLogic.Actions (
+>   toNand, toNor, truthTree,
+>   and, or, implies, iff, nand, nor, isConsistent,
+>   truthTableStrs, truthTableValues) 
+> where
+
+> import Prelude hiding (and, or)
+> import Text.Printf
+> import Data.List (union)
+
+> import WeberLogic.Parser
+
+> instance Show Letter where
+>     show exp =
+>         case exp of
+>             Name a          -> [a]
+>             Variable a      -> [a]
+
+> instance Eq Letter where
+>     (==) exp1 exp2 =
+>         case (exp1, exp2) of
+>             (Name a, Name b)         -> a == b
+>             (Variable a, Variable b) -> a == b
+>             (_, _)                   -> False   
+
+> instance Show LogicExp where
+>     show exp =
+>         case exp of
+>             Not a           -> printf "~%s" (show a)
+>             Or a b          -> printf "(%s+%s)" (show a) (show b)
+>             Xor a b         -> printf "(%s⊕%s)" (show a) (show b)
+>             And a b         -> printf "(%s&%s)" (show a) (show b)
+>             Implies a b     -> printf "(%s->%s)" (show a) (show b)
+>             Iff a b         -> printf "(%s<->%s)" (show a) (show b)
+>             Nand a b        -> printf "(%s|%s)" (show a) (show b)
+>             Nor a b         -> printf "(%s/%s)" (show a) (show b)
+>             Predicate a bs  -> printf "%c%s" a $ concatMap (show) bs
+ 
+> instance Eq LogicExp where
+>     (==) exp1 exp2 =
+>         case (exp1, exp2) of
+>             (Predicate a as, Predicate b bs) -> a == b && as == bs
+>             (Not a, Not b)                   -> a == b
+>             (Or a b, Or c d)                 -> a == c && b == d
+>             (Xor a b, Xor c d)               -> a == c && b == d
+>             (And a b, And c d)               -> a == c && b == d
+>             (Implies a b, Implies c d)       -> a == c && b == d
+>             (Iff a b, Iff c d)               -> a == c && b == d
+>             (Nand a b, Nand c d)             -> a == c && b == d
+>             (Nor a b, Nor c d)               -> a == c && b == d
+>             (_, _)                           -> False
+
+ 
+> lmap :: (LogicExp -> LogicExp) -> LogicExp -> LogicExp
+> lmap f exp =
+>     case exp of 
+>         Not a          -> f $ Not (lmap f a)
+>         Or a b         -> f $ Or (lmap f a) (lmap f b)
+>         And a b        -> f $ And (lmap f a) (lmap f b)
+>         Xor a b        -> f $ Xor (lmap f a) (lmap f b)
+>         Implies a b    -> f $ Implies (lmap f a) (lmap f b)
+>         Iff a b        -> f $ Iff (lmap f a) (lmap f b)
+>         Nand a b       -> f $ Nand (lmap f a) (lmap f b)
+>         Nor a b        -> f $ Nor (lmap f a) (lmap f b)
+>         Predicate a bs -> f exp 
+ 
+> toNand :: LogicExp -> LogicExp
+> toNand exp = lmap (toNand') exp
+>     where toNand' e = case e of
+>             Not a       -> a `Nand` a
+>             Or a b      -> (a `Nand` a) `Nand` (b `Nand` b)
+>             And a b     -> (a `Nand` b) `Nand` (a `Nand` b)
+>             Nand a b    -> a `Nand` b
+>             Nor a b     -> ((a `Nand` a) `Nand` (b `Nand` b)) `Nand` 
+>                                ((a `Nand` a) `Nand` (b `Nand` b))
+>             Implies a b -> toNand $ Or (toNand $ Not a) b
+>             Iff a b     -> toNand $ (a `Implies` b) `And` (b `Implies` a)
+>             _           -> e
+ 
+> toNor :: LogicExp -> LogicExp
+> toNor exp = lmap (toNor') exp
+>     where toNor' e = case e of
+>             Not a       -> a `Nor` a
+>             Or a b      -> (a `Nor` b) `Nor` (a `Nor` b)
+>             And a b     -> (a `Nor` a) `Nor` (b `Nor` b)
+>             Nor a b     -> a `Nor` b
+>             Nand a b    -> ((a `Nor` a) `Nor` (b `Nor` b)) `Nor` 
+>                                ((a `Nor` a) `Nor` (b `Nor` b))
+>             Implies a b -> toNor $ Or (toNor $ Not a) b
+>             Iff a b     -> toNor $ (a `Implies` b) `And` (b `Implies` a)
+>             _           -> e
+ 
+ 
+> decompose :: [LogicExp] -> [[LogicExp]]
+> decompose es = decompose' es []
+ 
+> decompose' :: [LogicExp] -> [LogicExp] -> [[LogicExp]]
+> decompose' exps as 
+>     | null exps = [as]
+>     | otherwise = let (e:es) = exps
+>         in case e of
+>            Predicate _ _      -> decompose' es (e:as)
+>            Not(Predicate _ _) -> decompose' es (e:as)
+>            And x y            -> decompose' (x:y:es) as 
+>            Or x y             -> (decompose' (x:es) as) ++ (decompose' (y:es) as)
+>            Implies x y        -> (decompose' ((Not x):es) as) ++ (decompose' (y:es) as)
+>            Iff x y            -> decompose' (Or (And x y) (And (Not x) (Not y)):es) as
+>            Not(And x y)       -> (decompose' ((Not x):es) as) ++ (decompose' ((Not y):es) as)
+>            Not(Or x y)        -> decompose' ((Not x):(Not y):es) as 
+>            Not(Implies x y)   -> decompose' ((And x (Not y)):es) as
+>            Not(Iff x y)       -> decompose' (Or (And x y) (And (Not x) (Not y)):es) as
+ 
+> isConsistent :: [LogicExp] -> Bool
+> isConsistent es = isConsistent' es []
+ 
+> isConsistent' :: [LogicExp] -> [LogicExp] -> Bool
+> isConsistent' exps as 
+>     | null exps = True
+>     | otherwise = let (e:es) = exps
+>         in case e of
+>            Predicate _ _       -> if elem (Not e) as then False else isConsistent' es (e:as)
+>            Not(Predicate x xs) -> if elem (Predicate x xs) as then False else isConsistent' es (e:as)
+>            And x y             -> isConsistent' (x:y:es) as 
+>            Or x y              -> (isConsistent' (x:es) as) || (isConsistent' (y:es) as)
+>            Implies x y         -> (isConsistent' ((Not x):es) as) || (isConsistent' (y:es) as)
+>            Iff x y             -> isConsistent' (Or (And x y) (And (Not x) (Not y)):es) as
+>            Not(And x y)        -> (isConsistent' ((Not x):es) as) || (isConsistent' ((Not y):es) as)
+>            Not(Or x y)         -> isConsistent' ((Not x):(Not y):es) as 
+>            Not(Implies x y)    -> isConsistent' ((And x (Not y)):es) as
+>            Not(Iff x y)        -> isConsistent' (Or (And x y) (And (Not x) (Not y)):es) as
+ 
+> truthTree :: [LogicExp] -> IO()
+> truthTree es = do 
+>         printf "%s\n" $ show es 
+>         truthTree' es [] 0
+ 
+> truthTree' :: [LogicExp] -> [LogicExp] -> Int -> IO()
+> truthTree' exps as indent = do
+>   if null exps 
+>   then print "Open" indent
+>   else let (e:es) = exps
+>     in do 
+>       print (show e) indent
+>       case e of
+>         Predicate x xs      -> if elem (Not e) as 
+>                              then print "Closed" indent
+>                              else truthTree' es (e:as) indent
+> 
+>         Not(Predicate x xs) -> if elem (Predicate x xs) as 
+>                              then print "Closed" indent
+>                              else truthTree' es (e:as) indent
+> 
+>         Not(Not x)       -> truthTree' (x:es) as indent
+> 
+>         And x y          -> truthTree' (x:y:es) as indent
+> 
+>         Or x y           -> do 
+>                               truthTree' (x:es) as (indent+1)
+>                               truthTree' (y:es) as (indent+1)
+> 
+>         Implies x y      -> let z = Or (Not x) (y)
+>                               in truthTree' (z:es) as indent
+> 
+>         Iff x y          -> let z = Or (And x y) (And (Not x) (Not y)) 
+>                               in truthTree' (z:es) as indent
+> 
+>         Not(And x y)     -> let z = Or (Not x) (Not y) 
+>                               in truthTree' (z:es) as indent
+> 
+>         Not(Or x y)      -> let z = And (Not x) (Not y) 
+>                               in truthTree' (z:es) as indent
+> 
+>         Not(Implies x y) -> let z = Or (Not x) y
+>                               in truthTree' (z:es) as indent
+> 
+>         Not(Iff x y)     -> let z = Or (And x y) (And (Not x) (Not y))
+>                               in truthTree' (z:es) as indent
+> 
+>     where print str indent = printf "%s%s\n" (replicate (indent*2) ' ') str
+ 
+> evalutateBinary :: (Bool -> Bool -> Bool) -> LogicExp -> LogicExp -> 
+>                    [(LogicExp, Bool)] -> Bool
+> evalutateBinary operator exp1 exp2 xs = exp1' `operator` exp2'
+>     where exp1' = evaluate exp1 xs;
+>           exp2' = evaluate exp2 xs
+           
+> evaluate :: LogicExp -> [(LogicExp, Bool)] -> Bool
+> evaluate exp xs =
+>     case exp of 
+>         Predicate a as -> if exp == c then v else evaluate exp xs'
+>                           where ((c,v):xs') = xs
+>         Not a          -> not $ evaluate a xs
+>         And a b        -> evalutateBinary and a b xs
+>         Or a b         -> evalutateBinary or a b xs
+>         Xor a b        -> evalutateBinary xor a b xs
+>         Nand a b       -> evalutateBinary nand a b xs
+>         Nor a b        -> evalutateBinary nor a b xs
+>         Implies a b    -> evalutateBinary implies a b xs
+>         Iff a b        -> evalutateBinary iff a b xs
+ 
+> and :: Bool -> Bool -> Bool
+> and True True = True
+> and _    _    = False
+ 
+> or :: Bool -> Bool -> Bool
+> or True _    = True
+> or _    True = True
+> or _    _    = False
+ 
+> implies :: Bool -> Bool -> Bool
+> implies True False = False
+> implies _    _     = True
+ 
+> iff :: Bool -> Bool -> Bool
+> iff True  True  = True
+> iff False False = True
+> iff _     _     = False
+ 
+> xor :: Bool -> Bool -> Bool
+> xor False False = False
+> xor True  True  = False
+> xor _     _     = True
+ 
+> nand :: Bool -> Bool -> Bool
+> nand x y = not (x `and` y)
+ 
+> nor :: Bool -> Bool -> Bool
+> nor x y = not (x `or` y)
+ 
+> truthTableStrs :: LogicExp -> [String]
+> truthTableStrs exp = 
+>   let (predicates, values, results) = truthTableValues exp 
+>       header_lhs = concatMap (printf "%-5s " . show) predicates
+>       header_rhs = printf "| %-5s" $ show exp 
+>       header     = header_lhs ++ header_rhs
+>       rows_lhs   = map (concatMap (printf "%-5s " . show)) values
+>       rows_rhs   = map (printf "| %-5s" . show) results
+>       rows       = zipWith (++) rows_lhs rows_rhs
+>   in header : rows
+
+> truthTableValues :: LogicExp -> ([LogicExp], [[Bool]], [Bool])
+> truthTableValues exp = 
+>   let (_, _, preds) = getBasics exp
+>       pred_values   = map (zip preds) (perm (length preds) [True, False])
+>       values        = map (map (snd)) pred_values
+>       results       = map (evaluate exp) pred_values
+>   in (preds, values, results)
+ 
+> perm i xs | i > 0 = [ x:ys | x <- xs, ys <- perm (i-1) xs]
+>           | otherwise = [[]]
+ 
+> --                       ([Names],  [Variables], [Predicates])
+> getBasics :: LogicExp -> ([Letter], [Letter], [LogicExp])
+> getBasics exp = 
+>     case exp of 
+>         Predicate a bs -> foldl sumTuples ([], [], [exp]) $ map toTuple bs
+>             where toTuple p = case p of
+>                     Name a     -> ([p], [], [])
+>                     Variable a -> ([], [p], [])
+>         Not a          -> getBasics a
+>         Nor a b        -> sumTuples (getBasics a) (getBasics b)
+>         Nand a b       -> sumTuples (getBasics a) (getBasics b)
+>         And a b        -> sumTuples (getBasics a) (getBasics b)
+>         Or a b         -> sumTuples (getBasics a) (getBasics b)
+>         Xor a b        -> sumTuples (getBasics a) (getBasics b)
+>         Iff a b        -> sumTuples (getBasics a) (getBasics b)
+>         Implies a b    -> sumTuples (getBasics a) (getBasics b)
+>     where sumTuples (xs1, xs2,  xs3) (ys1, ys2, ys3) = 
+>             ((xs1 `union` ys1), (xs2 `union` ys2), (xs3 `union` ys3))
diff --git a/WeberLogic/Parser.lhs b/WeberLogic/Parser.lhs
new file mode 100644
--- /dev/null
+++ b/WeberLogic/Parser.lhs
@@ -0,0 +1,148 @@
+> module WeberLogic.Parser (
+>   Letter(Name, Variable), 
+>   LogicExp(
+>     Not, Or, Xor, And, Implies, Iff, Nand, Nor, Predicate, Universal,
+>     Existential),
+>   parseExp, parseArg) 
+> where 
+
+> import Prelude hiding (and, or)
+> import Data.List (union)
+> import Text.Printf
+> import Text.Parsec as Parsec
+> import Text.Parsec hiding (Error)
+> import Text.Parsec.String
+> import Text.Parsec.Expr
+> import Text.Parsec.Token
+> import Text.Parsec.Language
+> import qualified Data.List as List
+
+> data Letter
+>     = Name Char
+>     | Variable Char
+
+> data LogicExp
+>     = Not LogicExp
+>     | Or LogicExp LogicExp
+>     | Xor LogicExp LogicExp
+>     | And LogicExp LogicExp
+>     | Implies LogicExp LogicExp
+>     | Iff LogicExp LogicExp
+>     | Nand LogicExp LogicExp
+>     | Nor LogicExp LogicExp
+>     | Predicate Char [Letter]
+>     | Universal Letter LogicExp
+>     | Existential LogicExp
+
+> parseExp :: Parser LogicExp
+> parseExp = do x <- parseExp1
+>               eof
+>               return x
+
+> parseExp1 :: Parser LogicExp
+> parseExp1 = try $ do
+>            x  <- parseExp2
+>            x' <- parseExp1' x
+>            return x'
+
+> parseExp1' :: LogicExp -> Parser LogicExp
+> parseExp1' x = try $ do
+>            string "<->"
+>            y <- parseExp2
+>            return $ Iff x y
+>         <|> do
+>            return x
+
+> parseExp2 :: Parser LogicExp
+> parseExp2 = try $ do
+>             x  <- parseExp3
+>             x' <- parseExp2' x
+>             return x'
+
+> parseExp2' :: LogicExp -> Parser LogicExp
+> parseExp2' x = try $ do
+>                string "->"
+>                y <- parseExp2
+>                return $ Implies x y
+>             <|> do
+>                return x
+ 
+> parseExp3 :: Parser LogicExp
+> parseExp3 = try $ do 
+>             lhs <- parseExp4
+>             rhs <- parseExp3' lhs
+>             return rhs
+>          <|> do 
+>             lhs <- parseExp4
+>             return lhs
+ 
+ 
+> parseOperator3 :: (LogicExp -> LogicExp -> LogicExp) -> 
+>                     String -> LogicExp -> Parser (LogicExp)
+> parseOperator3 connective symbol lhs
+>     = try $ do
+>         string symbol
+>         rhs <- parseExp4
+>         exp2 <- parseExp3' $ connective lhs rhs
+>         return exp2
+ 
+> parseExp3' :: LogicExp -> Parser (LogicExp)
+> parseExp3' lhs =  parseOperator3 And "&" lhs
+>               <|> parseOperator3 Or "+" lhs
+>               <|> parseOperator3 Nand "|" lhs
+>               <|> parseOperator3 Nor  "/" lhs
+>               <|> parseOperator3 Xor "⊕" lhs
+>               <|> do
+>                     return lhs
+ 
+> parseExp4 :: Parser LogicExp
+> parseExp4 = try $ do
+>             string "~"
+>             x <- parseExp4
+>             return $ Not x
+>          <|> (try $ do
+>             p <- upper
+>             xs <- parsePredicateLetters
+>             return $ Predicate p xs)
+>          <|> do
+>             char '('
+>             x <- parseExp1
+>             char ')'
+>             return $ x
+ 
+> parsePredicateLetters :: Parser ([Letter])
+> parsePredicateLetters
+>           = try $ do
+>               x <- oneOf "abcefghijklmnopqrst"
+>               xs <- parsePredicateLetters 
+>               return ((Name x):xs)
+>          <|> (try $ do
+>               x <- oneOf "uvwxyz"
+>               xs <- parsePredicateLetters 
+>               return ((Variable x):xs))
+>          <|> do
+>               return []
+
+> parseArg :: Parser [LogicExp]
+> parseArg = try $ do
+>              xs <- parseArg'
+>              return xs
+>          <|> do 
+>              x <- parseExp1
+>              spaces
+>              xs <- parseArg'
+>              return $ x : xs
+
+> parseArg' :: Parser [LogicExp]
+> parseArg' = try $ do
+>              string "|-"
+>              spaces
+>              x <- parseExp1
+>              return [x]
+>          <|> do 
+>              char ','
+>              spaces
+>              x <- parseExp1
+>              spaces
+>              xs <- parseArg'
+>              return $ x : xs