Maintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Portability : non-portable
Isabelle theorem prover for THF0
refuteProver, sledgehammerProver ) where
pfun :: String -> ProverFuncs
pfun tool = ProverFuncs {
cfgTimeout = maybe 20 (+ 10) . timeLimit,
proverCommand = \ tout tmpFile _ ->
return ("time", ["isabelle", tool, show (tout - 10), tmpFile]),
getMessage = \ res' pout _ ->
if null res' then concat $ filter (isPrefixOf "*** ") (lines pout)
getTimeUsed = \ line -> case fromMaybe "" $ stripPrefix "real\t" line of
s -> let sp p str = case dropWhile p str of
where (w, s'') = break p s'
(m : secs : _) = sp (== 'm') s
in Just $ read m * 60 + read secs }
createIsaSZSProver :: String -> String -> ProverFuncs -> ProverType
createIsaSZSProver = createSZSProver "isabelle"
isaProver = createIsaSZSProver "Isabelle (automated)"
"Automated Isabelle calling all tools available"
$ pfun "tptp_isabelle_demo"
nitpickProver :: ProverType
nitpickProver = createIsaSZSProver "Isabelle (nitpick)"
"Nitpick for TPTP problems"
refuteProver :: ProverType
refuteProver = createIsaSZSProver "Isabelle (refute)"
"refute for TPTP problems"
sledgehammerProver :: ProverType
sledgehammerProver = createIsaSZSProver "Isabelle (sledgehammer)"
"sledgehammer for TPTP problems"
$ pfun "tptp_sledgehammer"