934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuCopyright : (c) Domink Luecke, Uni Bremen 2009-2010
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuLicense : GPLv2 or higher, see LICENSE.txt
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuMaintainer : luecke@informatik.uni-bremen.de
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuStability : provisional
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuPortability : non-portable
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuFact++ prover for OWL
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiumodule OWL2.ProveFact (factProver, factConsChecker) where
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiuimport qualified Common.Result as Result
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiuimport Data.Time (TimeOfDay, midnight)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu The Prover implementation. First runs the batch prover (with graphical
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu feedback), then starts the GUI prover.
45e34c7696f9dd6163686ff6798b33a126590fa2Felix Gabriel MancefactProver :: Prover Sign Axiom OWLMorphism ProfSub ProofTree
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederfactProver = (mkAutomaticProver "java" "Fact" topS factGUI
e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder factCMDLautomaticBatch)
0a65899b09e78455a94af9128455f6613441ab71cmaeder { proverUsable = checkOWLjar factProverJarS }
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederfactProverJarS :: String
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederfactProverJarS = "OWLFactProver.jar"
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederfactJarS :: String
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Invokes the generic prover GUI.
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiufactGUI :: String -- ^ theory name
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> Theory Sign Axiom ProofTree
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiufactGUI thName th freedefs =
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu genericATPgui (atpFun thName) True (proverName factProver) thName th
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu freedefs emptyProofTree
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu automatic command line interface to the Fact prover.
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Pellet specific functions are omitted by data type ATPFunctions.
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiufactCMDLautomaticBatch ::
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Bool -- ^ True means include proved theorems
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> Bool -- ^ True means save problem file
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> MVar (Result.Result [ProofStatus ProofTree])
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -- ^ used to store the result of the batch run
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> String -- ^ theory name
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> TacticScript -- ^ default tactic script
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> Theory Sign Axiom ProofTree -- ^ theory
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> IO (ThreadId, MVar ())
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu {- ^ fst: identifier of the batch thread for killing it
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu snd: MVar to wait for the end of the thread -}
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiufactCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu thName defTS th freedefs =
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu resultMVar (proverName factProver) thName
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu The Cons-Checker implementation.
45e34c7696f9dd6163686ff6798b33a126590fa2Felix Gabriel MancefactConsChecker :: ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederfactConsChecker = (mkConsChecker "Fact" topS consCheck)
0a65899b09e78455a94af9128455f6613441ab71cmaeder { ccUsable = checkOWLjar factJarS }
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Record for prover specific functions. This is used by both GUI and command
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu line interface.
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuatpFun :: String -- ^ theory name
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> ATPFunctions Sign Axiom OWLMorphism ProofTree ProverState
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuatpFun _ = ATPFunctions
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu { initialProverState = owlProverState
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , atpTransSenName = id -- transSenName,
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , atpInsertSentence = insertOWLAxiom
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , goalOutput = \ a b _ -> showOWLProblem a b
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , proverHelpText = "Fact++"
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , batchTimeEnv = "HETS_FACT_BATCH_TIME_LIMIT"
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , fileExtensions = FileExtensions { problemOutput = ".owl" -- owl-hets
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , proverOutput = ".fact"
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , theoryConfiguration = ".pconf" }
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , runProver = runFact
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , createProverOptions = extraOpts }
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Runs the Fact++ consistency checker.
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuconsCheck :: String
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> TacticScript
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> TheoryMorphism Sign Axiom OWLMorphism ProofTree
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> IO (CCStatus ProofTree)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiuconsCheck thName (TacticScript tl) tm freedefs = case tTarget tm of
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Theory sig nSens ->
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu let saveOWL = False
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu proverStateI = owlProverState sig (toNamedList nSens) freedefs
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu problemS = showOWLProblemS proverStateI
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu tmpFileName = basename thName ++ ".owl"
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu pStatus out tUsed = CCStatus
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu { ccResult = Nothing
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , ccProofTree = ProofTree $ out ++ "\n\n" ++ problemS
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , ccUsedTime = tUsed }
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu when saveOWL (writeFile tmpFileName problemS)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu res <- runTimedFact tmpFileName problemS Nothing
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu $ fromMaybe maxBound $ readMaybe tl
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu return $ case res of
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Just (b, ex_code, out, t_u) -> let pStat = pStatus out t_u in if b then
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu case ex_code of
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ExitFailure 10 -> pStat { ccResult = Just True }
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ExitFailure 20 -> pStat { ccResult = Just False}
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Nothing -> pStatus "Timeout" midnight
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiurunTimedFact :: FilePath -- ^ basename of problem file
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> String -- ^ problem content
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> Maybe String -- ^ entail content
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> Int -- ^ time limit in seconds
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiurunTimedFact tmpFileName prob mEnt tLimit = do
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu let hasEnt = isJust mEnt
e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder jar = if hasEnt then factProverJarS else factJarS
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu (progTh, toolPath) <- check4HetsOWLjar jar
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu hasJniLib <- doesFileExist $ "/lib/" ++ jlibName
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian Maeder (_, arch, _) <- executeProcess "uname" ["-m"] ""
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu withinDirectory toolPath $ do
7d4eceb7957ee92980360a3d721e82c5a48bb6a6Christian Maeder mJni <- fmap (lookup "HETS_JNI_LIBS") getEnvironment
7d4eceb7957ee92980360a3d721e82c5a48bb6a6Christian Maeder let jni = fromMaybe ("lib/native/" ++ trim arch) mJni
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu hasJni <- doesFileExist $ jni </> jlibName
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu if hasJni || hasJniLib then do
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu timeTmpFile <- getTempFile prob tmpFileName
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu let entailsFile = timeTmpFile ++ ".entail.owl"
7d4eceb7957ee92980360a3d721e82c5a48bb6a6Christian Maeder jargs = ["-Djava.library.path=" ++ jni
7d4eceb7957ee92980360a3d721e82c5a48bb6a6Christian Maeder | not hasJniLib || isJust mJni ]
7d4eceb7957ee92980360a3d721e82c5a48bb6a6Christian Maeder ++ ["-jar", jar, "file://" ++ timeTmpFile]
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ++ ["file://" ++ entailsFile | hasEnt ]
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Just entail -> writeFile entailsFile entail
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu t_start <- getHetsTime
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu mExit <- timeoutCommand tLimit "java" jargs
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu t_end <- getHetsTime
d05f3655a4e033724a0baf5f652cbe18500b10baChristian Maeder removeFile timeTmpFile
d05f3655a4e033724a0baf5f652cbe18500b10baChristian Maeder when hasEnt $ removeFile entailsFile
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu return $ fmap (\ (ex, out, err) ->
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu (True, ex, out ++ err, diffHetsTime t_end t_start)) mExit
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu else return $ Just (False, ExitSuccess, "no " ++ jlibName, midnight)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu else return $ Just (False, ExitSuccess, jar ++ " not found.", midnight)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Invocation of the Fact Prover.
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiurunFact :: ProverState
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu {- ^ logical part containing the input Sign and axioms and possibly
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu goals that have been proved earlier as additional axioms -}
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> GenericConfig ProofTree -- ^ configuration to use
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> Bool -- ^ True means save TPTP file
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> String -- ^ name of the theory in the DevGraph
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> Named Axiom -- ^ goal to prove
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -> IO (ATPRetval, GenericConfig ProofTree)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu -- ^ (retval, configuration with proof status and complete output)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae BungiurunFact sps cfg saveFact thName nGoal = do
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu let prob = showOWLProblemS sps
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu entail = showOWLProblemS
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu sps { initialState = [ nGoal {isAxiom = True } ] }
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu when saveFact $ do
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu writeFile tmpFileName prob
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu writeFile (tmpFileName ++ ".entail.owl") entail
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu mExit <- runTimedFact tmpFileName prob (Just entail) tLimit
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ((err, retval), output, tUsed) <- case mExit of
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Just (b, ex, output, t_u) -> if b then do
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu let outp = lines output
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu return (proofStat ex outp t_u, outp, t_u)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu else return ((ATPError output, defaultProofStatus), [], t_u)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu Nothing -> return
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ( (ATPTLimitExceeded, defaultProofStatus)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , [], midnight)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu return (err, cfg
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu { proofStatus = retval
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , resultOutput = output
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , timeUsed = tUsed
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu tLimit = fromMaybe 800 $ timeLimit cfg
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu goalSuffix = '_' : senAttr nGoal
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu tmpFileName = basename thName ++ goalSuffix ++ ".owl"
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu proofStat exitCode out tUsed = case exitCode of
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ExitFailure 10 -> (ATPSuccess, (provedStatus tUsed)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu { usedAxioms = map senAttr $ initialState sps })
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ExitFailure 20 -> (ATPSuccess, disProvedStatus)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ExitFailure _ -> ( ATPError (unlines ("Internal error." : out))
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , defaultProofStatus)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu ExitSuccess -> ( ATPError (unlines ("Internal error." : out))
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , defaultProofStatus)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu tScript = TacticScript $ show ATPTacticScript
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu { tsTimeLimit = configTimeLimit cfg
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu , tsExtraOpts = extraOpts cfg }
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu defaultProofStatus =
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu (openProofStatus (senAttr nGoal) (proverName factProver) emptyProofTree)
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu { tacticScript = tScript }
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu disProvedStatus = defaultProofStatus {goalStatus = Disproved}
934f126d5b9d809fcb74f01507483f133804af0eFrancisc Nicolae Bungiu provedStatus ut =
48dd1cb775b8a6ee70833f1f76ccc88caf29801cEugen Kuksa defaultProofStatus { goalStatus = Proved True
48dd1cb775b8a6ee70833f1f76ccc88caf29801cEugen Kuksa , usedTime = ut
48dd1cb775b8a6ee70833f1f76ccc88caf29801cEugen Kuksa , tacticScript = tScript }