Proof Simplification

From Event-B
Revision as of 17:38, 4 June 2009 by imported>Nicolas (New page: Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predica...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predicate p1 into p2 when p2 is never used afterwards, is a needless step. This development aims at getting rid of that kind of needless data contained in proof files.


TODO: complete