Hets - the Heterogeneous Tool Set

Copyright(c) (c) Otto-von-Guericke University of Magdeburg 2020
LicenseGPLv2 or higher, see LICENSE.txt
Maintainermscodescu@gmail.com
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

TPTP.ConsChecker

Description

 

Synopsis

Documentation

extras :: ProverBinary -> Bool -> String -> String Source #

consCheck Source #

Arguments

:: ProverBinary 
-> String 
-> TacticScript 
-> TheoryMorphism Sign Sentence Morphism ProofTree 
-> [FreeDefMorphism Sentence Morphism]

freeness constraints

-> IO (CCStatus ProofTree) 

Runs the Darwin service. The tactic script only contains a string for the time limit.