| Copyright | (c) Rainer Grabbe |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | needs POSIX |
| Safe Haskell | None |
SoftFOL.ProverState
Description
Data structures and initialising functions for Prover state and configurations.
Synopsis
- data SoftFOLProverState = SoftFOLProverState {}
- spassProverState :: Sign -> [Named SPTerm] -> [FreeDefMorphism SPTerm SoftFOLMorphism] -> SoftFOLProverState
- insertSentenceGen :: SoftFOLProverState -> Named SPTerm -> SoftFOLProverState
- showDFGProblem :: String -> SoftFOLProverState -> Named SPTerm -> [String] -> IO String
- showTPTPProblemM :: String -> SoftFOLProverState -> [String] -> IO String
- showTPTPProblem :: String -> SoftFOLProverState -> Named SPTerm -> [String] -> IO String
- showTPTPProblemAux :: String -> SoftFOLProverState -> Maybe (Named SPTerm) -> [String] -> IO String
- parseSPASSCommands :: [String] -> [SPSetting]
- getAxioms :: SoftFOLProverState -> [String]
Data structures
data SoftFOLProverState Source #
Constructors
| SoftFOLProverState | |
Fields | |
SoftFOL specific functions for prover GUI
Arguments
| :: Sign | SoftFOL signature |
| -> [Named SPTerm] | list of named SoftFOL terms containing axioms |
| -> [FreeDefMorphism SPTerm SoftFOLMorphism] | freeness constraints |
| -> SoftFOLProverState |
Creates an initial SoftFOL prover state with logical part.
Arguments
| :: SoftFOLProverState | prover state containing initial logical part |
| -> Named SPTerm | goal to add |
| -> SoftFOLProverState |
Inserts a named SoftFOL term into SoftFOL prover state.
Arguments
| :: String | theory name |
| -> SoftFOLProverState | prover state containing initial logical part |
| -> Named SPTerm | goal to print |
| -> [String] | extra options |
| -> IO String | formatted output of the goal |
Pretty printing SoftFOL goal in DFG format.
Arguments
| :: String | theory name |
| -> SoftFOLProverState | prover state containing initial logical part |
| -> [String] | extra options |
| -> IO String | formatted output of the goal |
Pretty printing SoftFOL-model-finding-problem in TPTP format.
Arguments
| :: String | theory name |
| -> SoftFOLProverState | prover state containing initial logical part |
| -> Named SPTerm | goal to print |
| -> [String] | extra options |
| -> IO String | formatted output of the goal |
Pretty printing SoftFOL goal in TPTP format.
Arguments
| :: String | theory name |
| -> SoftFOLProverState | prover state containing initial logical part |
| -> Maybe (Named SPTerm) | possible goal to print |
| -> [String] | extra options |
| -> IO String | formatted output of the goal |
Arguments
| :: [String] | SPASS command line options |
| -> [SPSetting] | parsed parameters and options |
Translates SPASS command line into [SPSetting]
getAxioms :: SoftFOLProverState -> [String] Source #
get all axioms possibly used in a proof