Hets - the Heterogeneous Tool Set

Copyright(c) Rainer Grabbe
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

TPTP.Prover.ProverState

Description

Data structures and initialising functions for Prover state and configurations.

Synopsis

Documentation

data ProverState Source #

Constructors

ProverState 

Fields

Instances

Eq ProverState Source # 

Methods

(==) :: ProverState -> ProverState -> Bool

(/=) :: ProverState -> ProverState -> Bool

Data ProverState Source # 

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 :: (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 # 
Show ProverState Source # 

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.

tptpProverState Source #

Arguments

:: Sign

TPTP signature

-> [Named Sentence]

list of named TPTP sentences containing axioms

-> [FreeDefMorphism Sentence Morphism]

freeness constraints

-> ProverState