| Copyright | (c) Heng Jiang Uni Bremen 2004-2007 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | needs POSIX |
| Safe Haskell | None |
SoftFOL.ProveDarwin
Description
Interface for the Darwin service, uses GUI.GenericATP. See http://spass.mpi-sb.mpg.de/ for details on SPASS, and http://combination.cs.uiowa.edu/Darwin/ for Darwin.
Synopsis
- darwinProver :: ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree
- darwinCMDLautomaticBatch :: Bool -> Bool -> MVar (Result [ProofStatus ProofTree]) -> String -> TacticScript -> Theory Sign Sentence ProofTree -> [FreeDefMorphism SPTerm SoftFOLMorphism] -> IO (ThreadId, MVar ())
- darwinConsChecker :: ProverBinary -> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
- runDarwinProcess :: String -> Bool -> String -> String -> String -> IO (String, [String], Int)
- data ProverBinary
- darwinExe :: ProverBinary -> String
- proverBinary :: ProverBinary -> String
- tptpProvers :: [ProverBinary]
- eproverOpts :: String -> String
Documentation
darwinProver :: ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree Source #
The Prover implementation. First runs the batch prover (with graphical feedback), then starts the GUI prover.
darwinCMDLautomaticBatch 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 | theory consisting of a signature and sentences |
| -> [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 Darwin prover.
Darwin specific functions are omitted by data type ATPFunctions.
darwinConsChecker :: ProverBinary -> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree Source #
Arguments
| :: String | binary name |
| -> Bool | save problem |
| -> String | options |
| -> String | filename without extension |
| -> String | problem |
| -> IO (String, [String], Int) |
data ProverBinary Source #
Instances
| Bounded ProverBinary Source # | |
Defined in SoftFOL.ProveDarwin | |
| Enum ProverBinary Source # | |
Defined in SoftFOL.ProveDarwin Methods succ :: ProverBinary -> ProverBinary pred :: ProverBinary -> ProverBinary toEnum :: Int -> ProverBinary fromEnum :: ProverBinary -> Int enumFrom :: ProverBinary -> [ProverBinary] enumFromThen :: ProverBinary -> ProverBinary -> [ProverBinary] enumFromTo :: ProverBinary -> ProverBinary -> [ProverBinary] enumFromThenTo :: ProverBinary -> ProverBinary -> ProverBinary -> [ProverBinary] | |
darwinExe :: ProverBinary -> String Source #
proverBinary :: ProverBinary -> String Source #
tptpProvers :: [ProverBinary] Source #
eproverOpts :: String -> String Source #