Hets - the Heterogeneous Tool Set

Copyright(c) Heng Jiang, Uni Bremen 2004-2007
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

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

Documentation

darwinProver :: ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree

The Prover implementation. First runs the batch prover (with graphical feedback), then starts the GUI prover.

darwinCMDLautomaticBatch

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.