[opentheory-users] New principle of constant definition
ramana at member.fsf.org
Fri Nov 7 17:25:09 UTC 2014
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...
More information about the opentheory-users