| Copyright | (c) (c) Otto-von-Guericke University of Magdeburg 2020 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | mscodescu@gmail.com |
| Stability | provisional |
| Portability | needs POSIX |
| Safe Haskell | None |
TPTP.ConsChecker
Description
Synopsis
- extras :: ProverBinary -> Bool -> String -> String
- consCheck :: ProverBinary -> String -> TacticScript -> TheoryMorphism Sign Sentence Morphism ProofTree -> [FreeDefMorphism Sentence Morphism] -> IO (CCStatus ProofTree)
- darwinConsChecker :: ProverBinary -> ConsChecker Sign Sentence Sublogic Morphism ProofTree
Documentation
extras :: ProverBinary -> Bool -> String -> String Source #
Arguments
| :: ProverBinary | |
| -> String | |
| -> TacticScript | |
| -> TheoryMorphism Sign Sentence Morphism ProofTree | |
| -> [FreeDefMorphism Sentence Morphism] | freeness constraints |
| -> IO (CCStatus ProofTree) |
Runs the Darwin service. The tactic script only contains a string for the time limit.