[opentheory-users] New principle of constant definition

[Ramana Kumar]

On Wed, Nov 5, 2014 at 11:21 PM, Rob Arthan <rda at lemma-one.com> wrote:

> The current ProofPower implementation allows the set to be empty
> and just stores the input theorem as a definition (of nothing) in that
> case. I think that is it how it is specified in the CakeML work too.
> Maybe Ramana could confirm that.
>

Yes. [In the terminology of that work, the input theorem will become a new
(though clearly conservative) axiom in the theory.]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141107/c7066851/attachment.html>