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
