Hets - the Heterogeneous Tool Set

Copyright(c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

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.

Synopsis

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.

compositionFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv

composition without creating new new edges