<html><head></head><body bgcolor="#FFFFFF"><div><span class="Apple-style-span" style="-webkit-tap-highlight-color: rgba(26, 26, 26, 0.296875); -webkit-composition-fill-color: rgba(175, 192, 227, 0.230469); -webkit-composition-frame-color: rgba(77, 128, 180, 0.230469); ">On 07/12/2011, at 20:01, Ramana Kumar <<a href="mailto:ramana.kumar@gmail.com">ramana.kumar@gmail.com</a>> wrote:</span></div><blockquote type="cite"><div><font class="Apple-style-span" color="#005001"><br></font><span>It would be worth thinking about how to do all that with opentheory.</span><br><span>I wouldn't want to compromise the goal of storing prover-independent</span><br><span>theories without a good reason, though...</span><br></div></blockquote><br><div>My concern is that the resulting system might forget things that can't be recovered.  Then it will never be usable as a theory storage mechanism.   Is it possible to create a faithful representation of what's there that does support getting back exactly what was put in, and to *then* work on forgetting stuff that doesn't belong in theories meant for sharing with other systems?</div><div><br></div><div>Michael</div></body></html>