{- | Description : Proofs in development graphs Copyright : (c) Otto-von-Guericke University of Magdeburg License : GPLv2 or higher, see LICENSE.txt Proofs in development graphs. Follows Sect. IV:4.4 of the CASL Reference Manual. See also /Heterogeneous specification and the heterogeneous tool set/ (<http://www.informatik.uni-bremen.de/~till/papers/habil.ps>), section 5.6. "Proofs.Proofs" contains data types for proofs "Proofs.EdgeUtils" and "Proofs.StatusUtils" contain utilities. The proof calculus for development graphs is contained in the following modules: "Proofs.InferBasic" rule /basic inference/ "Proofs.Global" rules /global decomposition/, /global subsumption/ "Proofs.Local" rules /local decomposition/, /local subsumption/ (these are derived rules in the calculus) "Proofs.Composition" various composition rules "Proofs.HideTheoremShift" rule /Hide-Theorem-Shift/ "Proofs.TheoremHideShift" rule /Theorem-Hide-Shift/ The remaining rules have not been implemented yet. -} module Proofs where