| Copyright | (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | non-portable(Logic) |
| Safe Haskell | None |
Proofs.Composition
Description
Composition rules in the development graphs calculus. Follows Sect. IV:4.4 of the CASL Reference Manual, while combining several rules into one.
- composition :: LibName -> LibEnv -> LibEnv
- compositionCreatingEdges :: LibName -> LibEnv -> LibEnv
- compositionFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
- compositionCreatingEdgesFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
Documentation
composition :: LibName -> LibEnv -> LibEnv
gets all unproven global theorem edges in the current development graph and checks, if they are a composition of a global theorem path. If so, the edge is proven, with the corresponding path as its proof basis. If there is more than one path, the first of them is arbitrarily taken.
compositionCreatingEdges :: LibName -> LibEnv -> LibEnv
creates new edges by composing all paths of global theorem edges in the current development graph. These new edges are proven global theorems with the morphism and the conservativity of the corresponding path. If a new edge is the proven version of a previsously existing edge, that edge is deleted.