diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 term-rewriting library -- basic first order term rewriting.
 
-Copyright (c) 2011-2017 by Martin Avanzini, Bertram Felgenhauer and
+Copyright (c) 2011-2019 by Martin Avanzini, Bertram Felgenhauer and
 Christian Sternagel.
 
 Permission is hereby granted, free of charge, to any person obtaining a
diff --git a/src/Data/Rewriting/Problem/Parse.hs b/src/Data/Rewriting/Problem/Parse.hs
--- a/src/Data/Rewriting/Problem/Parse.hs
+++ b/src/Data/Rewriting/Problem/Parse.hs
@@ -71,6 +71,7 @@
                                                                          Prob.weakRules = [] } ,
                                       Prob.variables  = [] ,
                                       Prob.symbols    = [] ,
+                                      Prob.signature  = Nothing,
                                       Prob.comment    = Nothing }
 
 
@@ -89,10 +90,12 @@
   parseDecls = many1 parseDecl
   parseDecl =  decl "VAR"       vars       (\ e p -> p {Prob.variables = e `union` Prob.variables p})
            <|> decl "THEORY"    theory     (\ e p -> p {Prob.theory = maybeAppend Prob.theory e p})
+           <|> decl "SIG"       signature  (\ e p -> p {Prob.signature = maybeAppend Prob.signature e p})
            <|> decl "RULES"     rules      (\ e p -> p {Prob.rules   = e, --FIXME multiple RULES blocks?
                                                         Prob.symbols = Rules.funsDL (Prob.allRules e) [] })
            <|> decl "STRATEGY"  strategy   (\ e p -> p {Prob.strategy = e})
            <|> decl "STARTTERM" startterms (\ e p -> p {Prob.startTerms = e})
+           <|> (decl "COMMENT"   comment   (\ e p -> p {Prob.comment = maybeAppend Prob.comment e p}) <?> "comment")
            <|> (par comment >>= modifyProblem . (\ e p -> p {Prob.comment = maybeAppend Prob.comment e p}) <?> "comment")
   decl name p f = try (par $ do
       lex $ string name
@@ -103,6 +106,14 @@
 vars :: (Stream s (Either ProblemParseError) Char) => WSTParser s [String]
 vars = do vs <- many (lex $ ident "()," [])
           return vs
+
+signature :: (Stream s (Either ProblemParseError) Char) => WSTParser s [(String,Int)]
+signature = many fundecl
+    where
+        fundecl = par (do
+            f  <- lex $ ident "()," []
+            ar <- lex (read <$> many1 digit)
+            return $ (f,ar))
 
 theory :: (Stream s (Either ProblemParseError) Char) => WSTParser s [Prob.Theory String String]
 theory = many thdecl where
diff --git a/src/Data/Rewriting/Problem/Pretty.hs b/src/Data/Rewriting/Problem/Pretty.hs
--- a/src/Data/Rewriting/Problem/Pretty.hs
+++ b/src/Data/Rewriting/Problem/Pretty.hs
@@ -26,13 +26,14 @@
 prettyWST :: (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
 prettyWST fun var prob =
     printWhen (sterms /= AllTerms) (block "STARTTERM" $ text "CONSTRUCTOR-BASED")
-    <$$> printWhen (strat /= Full) (block "STRATEGY" $ ppStrat strat)
-    <$$> maybeblock "THEORY" theory ppTheories
-    <$$> block "VAR" (ppVars $ variables prob)
-    <$$> block "RULES" (ppRules $ rules prob)
-    <$$> maybeblock "COMMENT" comment text
+    <> printWhen (strat /= Full) (block "STRATEGY" $ ppStrat strat)
+    <> maybeblock "THEORY" theory ppTheories
+    <> block "VAR" (ppVars $ variables prob)
+    <> maybeblock "SIG" signature ppSignature
+    <> block "RULES" (ppRules $ rules prob)
+    <> maybeblock "COMMENT" comment text
 
-  where block n pp = parens $ hang 3 $ text n <$$> pp
+  where block n pp = (parens $ (hang 3 $ text n <$$> pp) <> linebreak) <> linebreak
         maybeblock n f fpp = case f prob of
                                Just e -> block n (fpp e)
                                Nothing -> empty
@@ -45,6 +46,9 @@
         ppTheories thys = align $ vcat [ppThy thy | thy <- thys]
             where ppThy (SymbolProperty p fs) = block p (align $ fillSep [ fun f | f <- fs ])
                   ppThy (Equations rs)        = block "EQUATIONS" $ vcat [ppRule "==" r | r <- rs]
+
+        ppSignature sigs = align $ fillSep [ppSig sig | sig <- sigs]
+            where ppSig (f,i) = parens $ fun f <+> int i
 
         ppRules rp = align $ vcat ([ppRule "->" r | r <- strictRules rp]
                                    ++ [ppRule "->=" r | r <- weakRules rp])
diff --git a/src/Data/Rewriting/Problem/Type.hs b/src/Data/Rewriting/Problem/Type.hs
--- a/src/Data/Rewriting/Problem/Type.hs
+++ b/src/Data/Rewriting/Problem/Type.hs
@@ -39,6 +39,7 @@
                            , rules      :: RulesPair f v
                            , variables  :: [v]
                            , symbols    :: [f]
+                           , signature  :: Maybe [(f, Int)]
                            , comment    :: Maybe String} deriving (Show)
 
 allRules :: RulesPair f v -> [Rule f v]
@@ -52,6 +53,7 @@
            , rules = mapRulesPair ffun fvar (rules prob)
            , variables = P.map fvar (variables prob)
            , symbols = P.map ffun (symbols prob)
+           , signature = fmap (P.map (\(f, a) -> (ffun f, a))) (signature prob)
            , comment = comment prob}
               
 mapTheory :: (f -> f') -> (v -> v') -> Theory f v -> Theory f' v'
diff --git a/term-rewriting.cabal b/term-rewriting.cabal
--- a/term-rewriting.cabal
+++ b/term-rewriting.cabal
@@ -1,5 +1,5 @@
 name:          term-rewriting
-version:       0.3.0.1
+version:       0.4
 stability:     experimental
 author:        Martin Avanzini,
                Bertram Felgenhauer,