Proofs.hs

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