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.

Synopsis

Documentation

callMathServ Source #

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).

parseMathServOut Source #

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 #
Methods showsPrec :: Int -> MathServServices -> ShowS show :: MathServServices -> String showList :: [MathServServices] -> ShowS

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

Show MathServOperationTypes Source #
Methods showsPrec :: Int -> MathServOperationTypes -> ShowS show :: MathServOperationTypes -> String showList :: [MathServOperationTypes] -> ShowS

data MathServCall Source #

Record type for all needed data to do a MathServ call.

Constructors

MathServCall
Fields mathServService :: MathServServices Selected MathServ service mathServOperation :: MathServOperationTypes Selected MathServ operation problem :: String Problem to prove in TPTP format proverTimeLimit :: Int Time limit extraOptions :: Maybe String Extra options

data MathServResponse Source #

A MathServ response structure to be filled by parsing all rdf-objects returned by MathServ.

Constructors

MathServResponse
Fields foAtpResult :: Either String MWFoAtpResult timeResource :: MWTimeResource

Instances

Eq MathServResponse Source #
Methods (==) :: MathServResponse -> MathServResponse -> Bool (/=) :: MathServResponse -> MathServResponse -> Bool
Ord MathServResponse Source #
Methods compare :: MathServResponse -> MathServResponse -> Ordering (<) :: MathServResponse -> MathServResponse -> Bool (<=) :: MathServResponse -> MathServResponse -> Bool (>) :: MathServResponse -> MathServResponse -> Bool (>=) :: MathServResponse -> MathServResponse -> Bool max :: MathServResponse -> MathServResponse -> MathServResponse min :: MathServResponse -> MathServResponse -> MathServResponse
Show MathServResponse Source #
Methods showsPrec :: Int -> MathServResponse -> ShowS show :: MathServResponse -> String showList :: [MathServResponse] -> ShowS

data MWFoAtpResult Source #

Constructors

MWFoAtpResult
Fields proof :: MWFormalProof outputStr :: String systemStatus :: MWStatus systemStr :: String time :: MWTimeResource

Instances

Eq MWFoAtpResult Source #
Methods (==) :: MWFoAtpResult -> MWFoAtpResult -> Bool (/=) :: MWFoAtpResult -> MWFoAtpResult -> Bool
Ord MWFoAtpResult Source #
Methods compare :: MWFoAtpResult -> MWFoAtpResult -> Ordering (<) :: MWFoAtpResult -> MWFoAtpResult -> Bool (<=) :: MWFoAtpResult -> MWFoAtpResult -> Bool (>) :: MWFoAtpResult -> MWFoAtpResult -> Bool (>=) :: MWFoAtpResult -> MWFoAtpResult -> Bool max :: MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult min :: MWFoAtpResult -> MWFoAtpResult -> MWFoAtpResult
Show MWFoAtpResult Source #
Methods showsPrec :: Int -> MWFoAtpResult -> ShowS show :: MWFoAtpResult -> String showList :: [MWFoAtpResult] -> ShowS

data MWFormalProof Source #

Constructors

TstpCnfRefutation
Fields formalProof :: String proofOf :: MWProvingProblem calculus :: MWCalculus axioms :: String

Instances

Eq MWFormalProof Source #
Methods (==) :: MWFormalProof -> MWFormalProof -> Bool (/=) :: MWFormalProof -> MWFormalProof -> Bool
Ord MWFormalProof Source #
Methods compare :: MWFormalProof -> MWFormalProof -> Ordering (<) :: MWFormalProof -> MWFormalProof -> Bool (<=) :: MWFormalProof -> MWFormalProof -> Bool (>) :: MWFormalProof -> MWFormalProof -> Bool (>=) :: MWFormalProof -> MWFormalProof -> Bool max :: MWFormalProof -> MWFormalProof -> MWFormalProof min :: MWFormalProof -> MWFormalProof -> MWFormalProof
Show MWFormalProof Source #
Methods showsPrec :: Int -> MWFormalProof -> ShowS show :: MWFormalProof -> String showList :: [MWFormalProof] -> ShowS

data MWStatus Source #

Constructors

MWStatus
Fields solved :: Bool foAtpStatus :: FoAtpStatus

Instances

Eq MWStatus Source #
Methods (==) :: MWStatus -> MWStatus -> Bool (/=) :: MWStatus -> MWStatus -> Bool
Ord MWStatus Source #
Methods compare :: MWStatus -> MWStatus -> Ordering (<) :: MWStatus -> MWStatus -> Bool (<=) :: MWStatus -> MWStatus -> Bool (>) :: MWStatus -> MWStatus -> Bool (>=) :: MWStatus -> MWStatus -> Bool max :: MWStatus -> MWStatus -> MWStatus min :: MWStatus -> MWStatus -> MWStatus
Show MWStatus Source #
Methods showsPrec :: Int -> MWStatus -> ShowS show :: MWStatus -> String showList :: [MWStatus] -> ShowS

data FoAtpStatus Source #

Constructors

Solved SolvedStatus
Unsolved UnsolvedStatus

Instances

Eq FoAtpStatus Source #
Methods (==) :: FoAtpStatus -> FoAtpStatus -> Bool (/=) :: FoAtpStatus -> FoAtpStatus -> Bool
Ord FoAtpStatus Source #
Methods compare :: FoAtpStatus -> FoAtpStatus -> Ordering (<) :: FoAtpStatus -> FoAtpStatus -> Bool (<=) :: FoAtpStatus -> FoAtpStatus -> Bool (>) :: FoAtpStatus -> FoAtpStatus -> Bool (>=) :: FoAtpStatus -> FoAtpStatus -> Bool max :: FoAtpStatus -> FoAtpStatus -> FoAtpStatus min :: FoAtpStatus -> FoAtpStatus -> FoAtpStatus
Read FoAtpStatus Source #
Methods readsPrec :: Int -> ReadS FoAtpStatus readList :: ReadS [FoAtpStatus] readPrec :: ReadPrec FoAtpStatus readListPrec :: ReadPrec [FoAtpStatus]
Show FoAtpStatus Source #
Methods showsPrec :: Int -> FoAtpStatus -> ShowS show :: FoAtpStatus -> String showList :: [FoAtpStatus] -> ShowS

data SolvedStatus Source #

Constructors

CounterEquivalent
CounterSatisfiable
CounterTheorem
Equivalent
NoConsequence
Satisfiable
TautologousConclusion
Tautology
Theorem
Unsatisfiable
UnsatisfiableConclusion

Instances

Eq SolvedStatus Source #
Methods (==) :: SolvedStatus -> SolvedStatus -> Bool (/=) :: SolvedStatus -> SolvedStatus -> Bool
Ord SolvedStatus Source #
Methods compare :: SolvedStatus -> SolvedStatus -> Ordering (<) :: SolvedStatus -> SolvedStatus -> Bool (<=) :: SolvedStatus -> SolvedStatus -> Bool (>) :: SolvedStatus -> SolvedStatus -> Bool (>=) :: SolvedStatus -> SolvedStatus -> Bool max :: SolvedStatus -> SolvedStatus -> SolvedStatus min :: SolvedStatus -> SolvedStatus -> SolvedStatus
Read SolvedStatus Source #
Methods readsPrec :: Int -> ReadS SolvedStatus readList :: ReadS [SolvedStatus] readPrec :: ReadPrec SolvedStatus readListPrec :: ReadPrec [SolvedStatus]
Show SolvedStatus Source #
Methods showsPrec :: Int -> SolvedStatus -> ShowS show :: SolvedStatus -> String showList :: [SolvedStatus] -> ShowS

data UnsolvedStatus Source #

Constructors

Assumed
GaveUp
InputError
MemoryOut
ResourceOut
Timeout
Unknown
NoStatus

Instances

Eq UnsolvedStatus Source #
Methods (==) :: UnsolvedStatus -> UnsolvedStatus -> Bool (/=) :: UnsolvedStatus -> UnsolvedStatus -> Bool
Ord UnsolvedStatus Source #
Methods compare :: UnsolvedStatus -> UnsolvedStatus -> Ordering (<) :: UnsolvedStatus -> UnsolvedStatus -> Bool (<=) :: UnsolvedStatus -> UnsolvedStatus -> Bool (>) :: UnsolvedStatus -> UnsolvedStatus -> Bool (>=) :: UnsolvedStatus -> UnsolvedStatus -> Bool max :: UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus min :: UnsolvedStatus -> UnsolvedStatus -> UnsolvedStatus
Read UnsolvedStatus Source #
Methods readsPrec :: Int -> ReadS UnsolvedStatus readList :: ReadS [UnsolvedStatus] readPrec :: ReadPrec UnsolvedStatus readListPrec :: ReadPrec [UnsolvedStatus]
Show UnsolvedStatus Source #
Methods showsPrec :: Int -> UnsolvedStatus -> ShowS show :: UnsolvedStatus -> String showList :: [UnsolvedStatus] -> ShowS

data MWCalculus Source #

Constructors

AprosNDCalculus
OmegaNDCalculus
EpResCalc
SpassResCalc
StandardRes
OtterCalc
VampireResCalc
ZenonCalc
UnknownCalc

Instances

Eq MWCalculus Source #
Methods (==) :: MWCalculus -> MWCalculus -> Bool (/=) :: MWCalculus -> MWCalculus -> Bool
Ord MWCalculus Source #
Methods compare :: MWCalculus -> MWCalculus -> Ordering (<) :: MWCalculus -> MWCalculus -> Bool (<=) :: MWCalculus -> MWCalculus -> Bool (>) :: MWCalculus -> MWCalculus -> Bool (>=) :: MWCalculus -> MWCalculus -> Bool max :: MWCalculus -> MWCalculus -> MWCalculus min :: MWCalculus -> MWCalculus -> MWCalculus
Read MWCalculus Source #
Methods readsPrec :: Int -> ReadS MWCalculus readList :: ReadS [MWCalculus] readPrec :: ReadPrec MWCalculus readListPrec :: ReadPrec [MWCalculus]
Show MWCalculus Source #
Methods showsPrec :: Int -> MWCalculus -> ShowS show :: MWCalculus -> String showList :: [MWCalculus] -> ShowS

data MWTimeResource Source #

Constructors

MWTimeResource
Fields cpuTime :: TimeOfDay wallClockTime :: TimeOfDay

Instances

Eq MWTimeResource Source #
Methods (==) :: MWTimeResource -> MWTimeResource -> Bool (/=) :: MWTimeResource -> MWTimeResource -> Bool
Ord MWTimeResource Source #
Methods compare :: MWTimeResource -> MWTimeResource -> Ordering (<) :: MWTimeResource -> MWTimeResource -> Bool (<=) :: MWTimeResource -> MWTimeResource -> Bool (>) :: MWTimeResource -> MWTimeResource -> Bool (>=) :: MWTimeResource -> MWTimeResource -> Bool max :: MWTimeResource -> MWTimeResource -> MWTimeResource min :: MWTimeResource -> MWTimeResource -> MWTimeResource
Show MWTimeResource Source #
Methods showsPrec :: Int -> MWTimeResource -> ShowS show :: MWTimeResource -> String showList :: [MWTimeResource] -> ShowS