Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder, DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (ATP GUI)
Safe HaskellNone

SoftFOL.ProveMetis

Description

call metis prover

Synopsis

Documentation

metisProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree

The Prover implementation.

metisProveCMDLautomaticBatch

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 Metis prover.