[opentheory-users] the Unwanted namespace

[Ramana Kumar]

Can we make a comprehensive list of the kind of stuff we might want to
store in a theory package?
I suspect there will be different recovery methods suitable for
different kinds of data, and looking at the requirements will help see
if and how opentheory might have to be modified or extended.

- Tag-free theorems, definitions, low-level proofs.
: already handled by article format

- theory name and description and dependencies
: already handled by theory package format

- NUMERAL tags
: reconstructible on reading?

- Abbrev tags

- Other tags? (Such as?)
: An alternative approach might be to store terms in an article as-is
(with tags) and then have different processing options for cleaning up
an article like do-nothing, remove all tags, remove all of the
following tags, or even possibly introduce tags for a specific prover
(if they are inferable).

- theorem names
: could be stored in a separate file mapping names to statements?

- automatic rewrites
: could be stored in a separate file containing a list of theorems?

- parsing and printing rules, and overloads
: also could be in a separate file?

- derived rules and other functionality associated with a theory
  - tactics, provers/decision procedures
  - syntax manipulation functions
  - what else?
: again, could be in a separate file of code, possibly using
opentheory article format to interface with the required
constants/theorems in the theory?

- what else?

At the moment it looks like almost everything could be handled by
extra files that would be mentioned in a theory package but wouldn't
interfere with article files in their current form. Only tag constants
are a problem because they change the terms the article is dealing
with.

Are there examples of tags that are definitely not reconstructible if
they are thrown away during cleanup?


On Thu, Dec 8, 2011 at 9:50 AM, Michael Norrish
<michael.norrish at nicta.com.au> wrote:
> 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
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>