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

SoftFOL.ProveSPASS

Description

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

Synopsis

spassProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree
spassProveCMDLautomaticBatch :: Bool -> Bool -> MVar (Result [ProofStatus ProofTree]) -> String -> TacticScript -> Theory Sign Sentence ProofTree -> [FreeDefMorphism SPTerm SoftFOLMorphism] -> IO (ThreadId, MVar ())

Documentation

spassProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree Source #

spassProveCMDLautomaticBatch 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 `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.