Copyright | (c) Rainer Grabbe DFKI GmbH |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | unknown |
Safe Haskell | None |
SoftFOL.MathServParsing
Description
Functions for parsing MathServ output into a MathServResponse structure.
- callMathServ :: MathServCall -> IO (Either String String)
- parseMathServOut :: Either String String -> IO (Either String MathServResponse)
- data MathServServices
- data MathServOperationTypes
- data MathServCall = MathServCall {
- mathServService :: MathServServices
- mathServOperation :: MathServOperationTypes
- problem :: String
- proverTimeLimit :: Int
- extraOptions :: Maybe String
- data MathServResponse = MathServResponse {
- foAtpResult :: Either String MWFoAtpResult
- timeResource :: MWTimeResource
- data MWFoAtpResult = MWFoAtpResult {
- proof :: MWFormalProof
- outputStr :: String
- systemStatus :: MWStatus
- systemStr :: String
- time :: MWTimeResource
- data MWFormalProof = TstpCnfRefutation {
- formalProof :: String
- proofOf :: MWProvingProblem
- calculus :: MWCalculus
- axioms :: String
- data MWStatus = MWStatus {
- solved :: Bool
- foAtpStatus :: FoAtpStatus
- data FoAtpStatus
- data SolvedStatus
- data UnsolvedStatus
- data MWCalculus
- data MWTimeResource = MWTimeResource {
- cpuTime :: TimeOfDay
- wallClockTime :: TimeOfDay
Documentation
Arguments
:: MathServCall | needed data to do a MathServ call |
-> IO (Either String String) | Left (SOAP error) or Right (MathServ output or error message) |
Sends a problem in TPTP format to MathServ using a given time limit. Either MathServ output is returned or a simple error message (no XML).
Arguments
:: Either String String | Left (SOAP error) or Right (MathServ output or error message) |
-> IO (Either String MathServResponse) | parsed rdf-objects in record |
Full parsing of RDF-objects returned by MathServ and putting the results into a MathServResponse data-structure.
data MathServServices Source #
MathServ services to select.
Constructors
Broker | Broker service |
VampireService | Vampire service |
Instances
Show MathServServices Source # | |
data MathServOperationTypes Source #
MathServ operation to select. These are only common types and will be translated into correct MathServOperations.
Constructors
ProblemOpt | stands for ProveProblemOpt |
ProblemChoice | stands for ProveProblemChoice |
TPTPProblem | stands for ProveTPTPProblem or ProveTPTPProblemWithOptions |
Problem | stands for ProveProblem |
Instances
data MathServCall Source #
Record type for all needed data to do a MathServ call.
Constructors
MathServCall | |
Fields
|
data MathServResponse Source #
A MathServ response structure to be filled by parsing all rdf-objects returned by MathServ.
Constructors
MathServResponse | |
Fields
|
Instances
Eq MathServResponse Source # | |
Ord MathServResponse Source # | |
Show MathServResponse Source # | |
data MWFoAtpResult Source #
Constructors
MWFoAtpResult | |
Fields
|
Instances
Eq MWFoAtpResult Source # | |
Ord MWFoAtpResult Source # | |
Show MWFoAtpResult Source # | |
data MWFormalProof Source #
Constructors
TstpCnfRefutation | |
Fields
|
Instances
Eq MWFormalProof Source # | |
Ord MWFormalProof Source # | |
Show MWFormalProof Source # | |
Constructors
MWStatus | |
Fields
|
data FoAtpStatus Source #
Constructors
Solved SolvedStatus | |
Unsolved UnsolvedStatus |
Instances
Eq FoAtpStatus Source # | |
Ord FoAtpStatus Source # | |
Read FoAtpStatus Source # | |
Show FoAtpStatus Source # | |
data SolvedStatus Source #
Constructors
CounterEquivalent | |
CounterSatisfiable | |
CounterTheorem | |
Equivalent | |
NoConsequence | |
Satisfiable | |
TautologousConclusion | |
Tautology | |
Theorem | |
Unsatisfiable | |
UnsatisfiableConclusion |
Instances
Eq SolvedStatus Source # | |
Ord SolvedStatus Source # | |
Read SolvedStatus Source # | |
Show SolvedStatus Source # | |
data UnsolvedStatus Source #
Constructors
Assumed | |
GaveUp | |
InputError | |
MemoryOut | |
ResourceOut | |
Timeout | |
Unknown | |
NoStatus |
Instances
Eq UnsolvedStatus Source # | |
Ord UnsolvedStatus Source # | |
Read UnsolvedStatus Source # | |
Show UnsolvedStatus Source # | |
data MWCalculus Source #
Constructors
AprosNDCalculus | |
OmegaNDCalculus | |
EpResCalc | |
SpassResCalc | |
StandardRes | |
OtterCalc | |
VampireResCalc | |
ZenonCalc | |
UnknownCalc |
Instances
Eq MWCalculus Source # | |
Ord MWCalculus Source # | |
Read MWCalculus Source # | |
Show MWCalculus Source # | |
data MWTimeResource Source #
Constructors
MWTimeResource | |
Fields
|
Instances
Eq MWTimeResource Source # | |
Ord MWTimeResource Source # | |
Show MWTimeResource Source # | |