Hets - the Heterogeneous Tool Set

Copyright(c) Eugen Kuksa University of Magdeburg 2017
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerEugen Kuksa <kuksa@iks.cs.ovgu.de>
Stabilityprovisional
Portabilitynon-portable (imports Logic)
Safe HaskellNone

TPTP.Prover.Common

Description

 

Documentation

type RunTheProverType Source #

Arguments

 = ProverState

logical part containing the input Sign and axioms and possibly goals that have been proved earlier as additional axioms

-> GenericConfig ProofTree

configuration to use

-> Bool

True means save TPTP file

-> String

name of the theory in the DevGraph

-> Named Sentence

goal to prove

-> IO (ATPRetval, GenericConfig ProofTree)

(retval, configuration with proof status and complete output)

mkTheoryFileName :: String -> Named Sentence -> String Source #

gnuTimeout :: IO String Source #

prepareProverInput :: ProverState -> GenericConfig ProofTree -> Bool -> String -> Named Sentence -> String -> IO String Source #

executeTheProver :: String -> [String] -> IO (ExitCode, [String], TimeOfDay) Source #

atpRetValAndProofStatus :: GenericConfig ProofTree -> Named Sentence -> TimeOfDay -> [String] -> String -> String -> (ATPRetval, ProofStatus ProofTree) Source #