On 01/09/17 15:12, Ken Kubota wrote: > Hi Mario, > > John has explained some of his motivation for HOL Light in an email > available online at […]
Thanks you. These links provide useful insight. > A HOL family tree with both HOL4 and HOL Light can be found at […] and at […]. Yes, I have read those papers. But they focus mostly on the foundational and not the user-level differences. > 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]. I see. It is good to know. But these differences are abstracted from the user who writes proofs using high-level tactics. I doubt that even at the level of applying inferences to the theorem data type through the OCaml or ML interface, it would make much difference whether –for example, “SUBST”– is primitive or derived. From the level of writing high-level proof scripts, is there any difference between the systems, apart from the choice of metalanguage/programming language (SML and OCaml) and the differences in the name of the identifiers of tactics? > 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. I thank you for your kindness and confidence. I am still studying the “well-known” formal systems of type theory. I have read chapter 1 of HOL4's “The HOL system LOGIC [For HOL Kananaskis-11]” and I am currently reading “Type Theory and Formal Proof: An Introduction” by R. Nederpelt and H. Geuvers (2014). Thus although I am interested, I shall turn down your kind offer because –right now– my background knowledge in type theory is very limited, and could neither make much use of the draft nor provide the feedback that is expected when sharing pre-publication drafts. I am fine waiting until your paper is ready as I have much to read of the same topic in the meantime. ☺ ----- Regards. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
