| 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 {}
- data MathServResponse = MathServResponse {}
- data MWFoAtpResult = MWFoAtpResult {}
- 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 {}
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
MathServ services to select.
Constructors
| Broker | Broker service |
| VampireService | Vampire service |
Instances
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
Record type for all needed data to do a MathServ call.
Constructors
| MathServCall | |
Fields
| |
data MathServResponse
A MathServ response structure to be filled by parsing all rdf-objects returned by MathServ.
Constructors
| MathServResponse | |
Fields | |
data MWFoAtpResult
Constructors
| MWFoAtpResult | |
Fields
| |
Instances
data MWFormalProof
Constructors
| TstpCnfRefutation | |
Fields
| |
Instances
data MWStatus
Constructors
| MWStatus | |
Fields
| |
data SolvedStatus
Constructors
| CounterEquivalent | |
| CounterSatisfiable | |
| CounterTheorem | |
| Equivalent | |
| NoConsequence | |
| Satisfiable | |
| TautologousConclusion | |
| Tautology | |
| Theorem | |
| Unsatisfiable | |
| UnsatisfiableConclusion |
Instances
data UnsolvedStatus
Constructors
| Assumed | |
| GaveUp | |
| InputError | |
| MemoryOut | |
| ResourceOut | |
| Timeout | |
| Unknown | |
| NoStatus |
data MWCalculus
Constructors
| AprosNDCalculus | |
| OmegaNDCalculus | |
| EpResCalc | |
| SpassResCalc | |
| StandardRes | |
| OtterCalc | |
| VampireResCalc | |
| ZenonCalc | |
| UnknownCalc |
Instances