[opentheory-users] names of theorems

[Joe Hurd]

Hi Ramana,

There are no theorem names in OpenTheory. One design goal of
OpenTheory is to minimize the use of names (which may change between
theorem prover implementations), and make sure that all names can be
easily renamed, which is why:

1. The interpret: tags in theory files can be used to rename theory
type operators and constants.

2. The opentheory tool outputs a warning if theories export theorems
with free (term) variables, and primitive inferences work modulo alpha
equivalence.

I lament the loss of a short mnemonic to refer to OpenTheory theorems,
but I expect that each theorem prover will maintain their own mapping
between OpenTheory theorem statements and local theorem names to
provide this feature to users.

Cheers,

Joe

On Mon, Jan 10, 2011 at 9:41 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> Does OpenTheory have any notion of a theorem's name?
> As far as I can see we have names for constants (including type
> operators) and theories (i.e. packages), but not theorems.
> I suppose the statement of the theorem is a good identifier in many
> ways, especially if there is good term matching software available.
> Natural language names can be mnemonic though.
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>