[opentheory-users] removing definitions from theories
ramana at member.fsf.org
Wed Feb 3 05:48:38 UTC 2016
Do you have any comments on the plan I described?
And/or would you be able to add the definition-removing functionality to
the opentheory tool?
On 30 January 2016 at 12:57, Ramana Kumar <ramana at member.fsf.org> wrote:
> I am trying to build a compatibility bridge between HOL4's standard
> library and the OpenTheory standard library.
> I've thought about (and started trying) various approaches.
> The latest idea (due mostly to Michael Norrish) is:
> 1. Record a theory containing the HOL4 standard library, entirely in
> the HOL4 namespace, depending only on the axioms of HOL.
> 2. Remove from this theory all definitions of things that are already
> in the OpenTheory standard library. The constants should then become
> ungrounded, and where they were defined the article should instead add the
> definitional axioms as axioms.
> 3. Instantiate all the ungrounded constants with constants from the
> OpenTheory standard library, and then also add the OpenTheory standard
> 4. Prove any remaining axioms.
> The feature I requested is for step 2. I realise now that I need to be
> able to remove definitions selectively, not just remove them all. There may
> be some way to accomplish that even if the primitive functionality is to
> remove them all, though.
> On 30 January 2016 at 03:52, Joe Leslie-Hurd <joe at gilith.com> wrote:
>> Hi Ramana,
>> There's currently no tool support for this, but I don't think it would
>> be too difficult to implement. What is your use-case?
>> On Fri, Jan 29, 2016 at 12:36 AM, Ramana Kumar <ramana at member.fsf.org>
>> > Hi,
>> > Is it possible to take a theory that makes definitions of
>> > and then re-present the same theory _without_ making the definitions
>> > (instead taking them as ungrounded constants, and the definitional
>> > as axioms).
>> > I know there is already this command:
>> > opentheory info --theorems ...
>> > which removes all the proofs, but it still keeps the definitions in.
>> > Can I also remove the definitions?
>> > In essence, I want a totally axiomatic presentation of a theory.
>> > Thanks,
>> > Ramana
>> > _______________________________________________
>> > opentheory-users mailing list
>> > opentheory-users at gilith.com
>> > http://www.gilith.com/opentheory/mailing-list
>> opentheory-users mailing list
>> opentheory-users at gilith.com
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the opentheory-users