| Copyright | (c) Eugen Kuksa University of Magdeburg 2017 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Eugen Kuksa <kuksa@iks.cs.ovgu.de> |
| Stability | provisional |
| Portability | non-portable (imports Logic) |
| Safe Haskell | None |
TPTP.Prover.Common
Description
Documentation
type AtpFunType = String -> ATPFunctions Sign Sentence Morphism ProofTree ProverState Source #
type RunTheProverType Source #
Arguments
| = ProverState | logical part containing the input Sign and axioms and possibly goals that have been proved earlier as additional axioms |
| -> GenericConfig ProofTree | configuration to use |
| -> Bool | True means save TPTP file |
| -> String | name of the theory in the DevGraph |
| -> Named Sentence | goal to prove |
| -> IO (ATPRetval, GenericConfig ProofTree) | (retval, configuration with proof status and complete output) |
mkProver :: String -> String -> Sublogic -> RunTheProverType -> Prover Sign Sentence Morphism Sublogic ProofTree Source #
mkTheoryFileName :: String -> Named Sentence -> String Source #
getTimeLimit :: GenericConfig ProofTree -> Int Source #
hardTimeLimit :: GenericConfig ProofTree -> Int Source #
gnuTimeout :: IO String Source #
prepareProverInput :: ProverState -> GenericConfig ProofTree -> Bool -> String -> Named Sentence -> String -> IO String Source #
executeTheProver :: String -> [String] -> IO (ExitCode, [String], TimeOfDay) Source #
atpRetValAndProofStatus :: GenericConfig ProofTree -> Named Sentence -> TimeOfDay -> [String] -> String -> String -> (ATPRetval, ProofStatus ProofTree) Source #
atpRetValAndProofStatus' :: GenericConfig ProofTree -> String -> TimeOfDay -> [String] -> String -> String -> (ATPRetval, ProofStatus ProofTree) Source #
selectRetValAndProofStatus :: (ProofStatus ProofTree, ProofStatus ProofTree, ProofStatus ProofTree) -> String -> (ATPRetval, ProofStatus ProofTree) Source #
proofStatuses :: GenericConfig ProofTree -> Named Sentence -> TimeOfDay -> [String] -> String -> (ProofStatus ProofTree, ProofStatus ProofTree, ProofStatus ProofTree) Source #
proofStatuses' :: GenericConfig ProofTree -> String -> TimeOfDay -> [String] -> String -> (ProofStatus ProofTree, ProofStatus ProofTree, ProofStatus ProofTree) Source #