Hets - the Heterogeneous Tool Set
Copyright(c) Otto-von-Guericke University of Magdeburg
LicenseGPLv2 or higher, see LICENSE.txt
Safe HaskellNone

HetsAPI.ProveCommands

Description

 
Synopsis

Documentation

getAvailableComorphisms :: G_theory -> [AnyComorphism] Source #

getAvailableComorphisms theory yields all available comorphisms for theory

getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)] Source #

getUsableProvers theory checks for usable provers available on the machine

getUsableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)] Source #

getUsableConsistencyCheckers theory checks for usable consistencey checkers for theory available on the machine

proveNode :: G_theory -> ProofOptions -> ResultT IO ProofResult Source #

proveNode theory prover comorphism proves all goals in theory using all all axioms in theory. If prover or comorphism is Nothing the first usable prover or comorphism, respectively, is used.

data ProofOptions Source #

Constructors

ProofOptions 

Fields

data ConsCheckingOptions Source #

Constructors

ConsCheckingOptions 

Fields