> Why did you ignore Google web search (www.google.com) and Google scholar > search (scholar.google.com)? DuckDuckGo is built-in supported by some open > source products, but I think it’s generally a garbage.
Google has a lot of private data about people. They can do, and do, many bad things with this data. I can not stop Google surveillance, but I do not want to make their task easier. Anyway, Startpage is an independent proxy for Google Search therefore the results should be similar to what Google Search would provide directly. In my experience DuckDuckGo has served well enough. It is my main search engine. Unfortunately, I still use Google Scholar because I have not found a good general purpose alternative. I use PubMed when I need to search for publications in medicine, but for mathematics/logic I do not know of any good alternative. Suggestions would be very welcome. > My experience: “HOL4” is a bad key word, because mostly what you may found is > a formalization done in old HOL versions. Instead, “formalization” + “higher > order logic” + domain keywords should be enough. Thanks! This gives much better results for my aforementioned benchmark test about prime numbers. ☺ There seems to be no signification formalization of elementary topology in HOL4. I am aware that there is some topology in “/src/real” in the HOl4 distribution, but it is very limited. Searching with DuckDuckGo, Startpage and Google Scholar for “formalization "higher order logic" topology” does not turn anything relevant. As my first development with a proof assistant I am formalizing some theorems of elementary topology in HOL4. I plan to develop and publish a theory which is suitable as the foundation for further developments. If you know of an existing formalization of elementary topology in HOL4 please let me know, so that I can avoid duplicating work. Regards. Note: It seems that you forgot to reply to the mailing list. On 10/09/17 13:34, Chun Tian (binghe) wrote: > Hi, > > Why did you ignore Google web search (www.google.com) and Google scholar > search (scholar.google.com)? DuckDuckGo is built-in supported by some open > source products, but I think it’s generally a garbage. > > My experience: “HOL4” is a bad key word, because mostly what you may found is > a formalization done in old HOL versions. Instead, “formalization” + “higher > order logic” + domain keywords should be enough. > > Regards, > > Chun Tian -- 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
