Copyright | (c) Rene Wagner, Klaus Luettich, Rainer Grabbe, Uni Bremen 2005-2006 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | needs POSIX |
Safe Haskell | None |
Interface for the MathServe broker which calls different ATP systems, uses GUI.GenericATP.
- mathServBroker :: Prover Sign Sentence SoftFOLMorphism () ProofTree
- mathServBrokerCMDLautomaticBatch :: Bool -> Bool -> MVar (Result [ProofStatus ProofTree]) -> String -> TacticScript -> Theory Sign Sentence ProofTree -> [FreeDefMorphism SPTerm SoftFOLMorphism] -> IO (ThreadId, MVar ())
Documentation
mathServBroker :: Prover Sign Sentence SoftFOLMorphism () ProofTree
The Prover implementation. First runs the batch prover (with graphical feedback), then starts the GUI prover.
mathServBrokerCMDLautomaticBatch
:: Bool | True means include proved theorems |
-> Bool | True means save problem file |
-> MVar (Result [ProofStatus ProofTree]) | used to store the result of the batch run |
-> String | theory name |
-> TacticScript | default tactic script |
-> Theory Sign Sentence ProofTree | |
-> [FreeDefMorphism SPTerm SoftFOLMorphism] | freeness constraints |
-> IO (ThreadId, MVar ()) | fst: identifier of the batch thread for killing it snd: MVar to wait for the end of the thread |
Implementation of proveCMDLautomaticBatch
which provides an
automatic command line interface to the MathServe Broker.
MathServ specific functions are omitted by data type ATPFunctions.