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.
- data ProverState = ProverState {
- psLogicalPart :: PLogicalPart
- getAxioms :: ProverState -> [String]
- insertSentenceIntoProverState :: ProverState -> Named Sentence -> ProverState
- ioShowTPTPProblem :: String -> ProverState -> Named Sentence -> [String] -> IO String
- tptpProverState :: Sign -> [Named Sentence] -> [FreeDefMorphism Sentence Morphism] -> ProverState
Documentation
data ProverState Source #
Constructors
ProverState | |
Fields
|
Instances
Eq ProverState Source # | |
Data ProverState Source # | |
Ord ProverState Source # | |
Show ProverState Source # | |
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 |
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.
Arguments
:: Sign | TPTP signature |
-> [Named Sentence] | list of named TPTP sentences containing axioms |
-> [FreeDefMorphism Sentence Morphism] | freeness constraints |
-> ProverState |