Copyright | (c) Otto-von-Guericke University of Magdeburg |
---|---|

License | GPLv2 or higher, see LICENSE.txt |

Safe Haskell | Safe |

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.