Hets - the Heterogeneous Tool Set
Copyright(c) Rene Wagner Klaus Luettich Rainer Grabbe
Uni Bremen 2005-2006
LicenseGPLv2 or higher, see LICENSE.txt
Portabilityneeds POSIX
Safe HaskellNone



Interface for the SPASS theorem prover, uses GUI.GenericATP. See http://spass.mpi-sb.mpg.de/ for details on SPASS.



spassProveCMDLautomaticBatch Source #


:: 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 Sign and a list of Named Sentence

-> [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 SPASS prover. SPASS specific functions are omitted by data type ATPFunctions.