| Safe Haskell | None |
|---|
HetsAPI.ProveCommands
Synopsis
- availableComorphisms :: G_theory -> [AnyComorphism]
- usableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
- usableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)]
- autoProveNode :: G_theory -> Maybe G_prover -> Maybe AnyComorphism -> ResultT IO (G_theory, ProofState, [ProofStatus G_proof_tree])
- proveNode :: Bool -> Int -> [String] -> [String] -> G_theory -> (G_prover, AnyComorphism) -> ResultT IO (ProofState, [ProofStatus G_proof_tree])
- checkConsistency :: Bool -> G_cons_checker -> AnyComorphism -> LibName -> LibEnv -> DGraph -> LNode DGNodeLab -> Int -> IO ConsistencyStatus
- checkConservativityNode :: LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory)
Documentation
availableComorphisms :: G_theory -> [AnyComorphism] Source #
availableComorphisms theory yields all available comorphisms for theory
usableProvers :: G_theory -> IO [(G_prover, AnyComorphism)] Source #
usableProvers theory checks for usable provers available on the machine
usableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)] Source #
usableConsistencyCheckers theory checks for usable consistencey checkers
for theory available on the machine
autoProveNode :: G_theory -> Maybe G_prover -> Maybe AnyComorphism -> ResultT IO (G_theory, ProofState, [ProofStatus G_proof_tree]) 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.
proveNode :: Bool -> Int -> [String] -> [String] -> G_theory -> (G_prover, AnyComorphism) -> ResultT IO (ProofState, [ProofStatus G_proof_tree]) Source #
proveNode sub timeout goals axioms theory (prover, comorphism) proves
goals with prover after applying comorphism. If goals is empty all
goals are selected. Same for axioms. If sub is set theorems are used in
subsequent proofs. The runtime is restricted by timeout.
checkConsistency :: Bool -> G_cons_checker -> AnyComorphism -> LibName -> LibEnv -> DGraph -> LNode DGNodeLab -> Int -> IO ConsistencyStatus Source #
checkConsistency includeTheorems cc comorphism libname libenv
dg node timeout first applies the comorphism cc to the theory at node
in the developmentGraph dg inside the library libname in the environment
libenv, then checks the consistency using the consistency checker cc
with a timeout of timeout seconds.
checkConservativityNode :: LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory) Source #