Safe Haskell | None |
---|

## 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 #