Copyright	(c) Rainer Grabbe
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	needs POSIX
Safe Haskell	None

TPTP.Prover.ProverState

Description

Data structures and initialising functions for Prover state and configurations.

Synopsis

data ProverState = ProverState {
- psLogicalPart :: PLogicalPart
}
getAxioms :: ProverState -> [String]
insertSentenceIntoProverState :: ProverState -> Named Sentence -> ProverState
ioShowTPTPProblem :: String -> ProverState -> Named Sentence -> [String] -> IO String
showTPTPProblemM :: String -> ProverState -> [String] -> IO String
tptpProverState :: Sign -> [Named Sentence] -> [FreeDefMorphism Sentence Morphism] -> ProverState

Documentation

data ProverState Source #

Constructors

ProverState
Fields psLogicalPart :: PLogicalPart

Instances

Instances details

Eq ProverState Source #
Instance details Defined in TPTP.Prover.ProverState Methods (==) :: ProverState -> ProverState -> Bool (/=) :: ProverState -> ProverState -> Bool
Data ProverState Source #
Instance details Defined in TPTP.Prover.ProverState Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProverState -> c ProverState gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProverState toConstr :: ProverState -> Constr dataTypeOf :: ProverState -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProverState) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProverState) gmapT :: (forall b. Data b => b -> b) -> ProverState -> ProverState gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProverState -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProverState -> r gmapQ :: (forall d. Data d => d -> u) -> ProverState -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProverState -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProverState -> m ProverState gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProverState -> m ProverState gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProverState -> m ProverState
Ord ProverState Source #
Instance details Defined in TPTP.Prover.ProverState Methods compare :: ProverState -> ProverState -> Ordering (<) :: ProverState -> ProverState -> Bool (<=) :: ProverState -> ProverState -> Bool (>) :: ProverState -> ProverState -> Bool (>=) :: ProverState -> ProverState -> Bool max :: ProverState -> ProverState -> ProverState min :: ProverState -> ProverState -> ProverState
Show ProverState Source #
Instance details Defined in TPTP.Prover.ProverState Methods showsPrec :: Int -> ProverState -> ShowS show :: ProverState -> String showList :: [ProverState] -> ShowS

getAxioms :: ProverState -> [String] Source #

gets all axioms possibly used in a proof

insertSentenceIntoProverState Source #

Arguments

:: ProverState	prover state containing initial logical part
-> Named Sentence	goal to add
-> ProverState

ioShowTPTPProblem Source #

Arguments

:: String	theory name
-> ProverState	prover state containing initial logical part
-> Named Sentence	goal to print
-> [String]	extra options
-> IO String	formatted output of the goal

Pretty printing TPTP goal in TPTP format.

showTPTPProblemM Source #

Arguments

:: String	theory name
-> ProverState	prover state containing initial logical part
-> [String]	extra options
-> IO String	formatted output of the goal

tptpProverState Source #

Arguments

:: Sign	TPTP signature
-> [Named Sentence]	list of named TPTP sentences containing axioms
-> [FreeDefMorphism Sentence Morphism]	freeness constraints
-> ProverState