[opentheory-users] the Unwanted namespace

[Michael Norrish]

On 07/12/2011, at 20:01, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 
> It would be worth thinking about how to do all that with opentheory.
> I wouldn't want to compromise the goal of storing prover-independent
> theories without a good reason, though...

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?

Michael
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20111208/6f53249f/attachment.htm>