| Copyright | (c) Christian Maeder DFKI GmbH 2010 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | non-portable (ATP GUI) |
| Safe Haskell | None |
SoftFOL.ProveMetis
Description
call metis prover
Synopsis
- metisProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree
- metisProveCMDLautomaticBatch :: Bool -> Bool -> MVar (Result [ProofStatus ProofTree]) -> String -> TacticScript -> Theory Sign Sentence ProofTree -> [FreeDefMorphism SPTerm SoftFOLMorphism] -> IO (ThreadId, MVar ())
Documentation
metisProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree Source #
The Prover implementation.
metisProveCMDLautomaticBatch Source #
Arguments
| :: 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 Metis prover.