Copyright | (c) Rainer Grabbe |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | needs POSIX |
Safe Haskell | None |
Data structures and initialising functions for Prover state and configurations.
- 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
SoftFOL specific functions for prover GUI
:: 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.
:: SoftFOLProverState | prover state containing initial logical part |
-> Named SPTerm | goal to add |
-> SoftFOLProverState |
Inserts a named SoftFOL term into SoftFOL prover state.
:: 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.
:: 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.
:: 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.
Translates SPASS command line into [SPSetting]
getAxioms :: SoftFOLProverState -> [String]
get all axioms possibly used in a proof