Hi Ken,
Feel free to ignore if I am mistaken, but I suspect from your message that
you are confusing me (Mario Carneiro) with the author of the HOL message (Mario
Castelán Castro).
Regards,
Mario Carneiro
On Sep 1, 2017 4:30 PM, "Ken Kubota" <m...@kenkubota.de> wrote:
Hi Mario,
John has explained some of his motivation for HOL Light in an email
available online at
https://sourceforge.net/p/hol/mailman/message/35444612/
Some more information can be found in his email at
https://sourceforge.net/p/hol/mailman/message/35446248/
A HOL family tree with both HOL4 and HOL Light can be found at
http://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf (p. 19)
in a text describing "HOL Light, a version with a sim-
plified axiomatization and rationalized structure", and at
http://www.owlofminerva.net/files/fom.pdf (p. 1).
What makes HOL Light special (in my opinion), is that it tries to
reduce the logic to a simpler logical core (hence, HOL "Light").
In this respect, it is very similar to the philosophy of Metamath and Q0/R0.
For this reason, I chose HOL Light as point of reference in my draft
describing R0, writing that "HOL Light […] has [only] 'ten primitive
rules of inference' [Harrison, 2009, p. 61]" [Kubota, 2015, p. 14].
Recalling our previous private communication, I could send you
the draft describing R0, if you are interested (for private use only,
please do not quote). I hope to publish a full description by the
end of the year.
Kind regards,
Ken Kubota
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100
> Am 30.08.2017 um 17:36 schrieb Mario Castelán Castro <
marioxcc...@yandex.com>:
>
> Hello.
>
> I know that HOL4 and HOL Light implement the same logic, and moreover
> they seem to have many tactics in common. I have only used (and I am
> still learning) HOL4, but I have looked at the documentation of HOL Light.
>
> What is the difference between for an user interesting in having his
> proofs computer-verified? What are the reasons to choose one of these
> systems instead of the other?
>
> Thanks.
>
> --
> Do not eat animals, respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
> ------------------------------------------------------------
------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot______
_________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------
------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
