I'd add to Ramana's list that HOL4 adds a very simple but powerful form of polymorphism to the system discussed in Bill Farmer's "The seven virtues of simple type theory".
Both PVS and Coq support dependent types which adds some extra expressiveness compared with the polymorphism in HOL4 at the expense of considerable complication in the logic. (I wouldn't describe either of these systems as "using higher order logic".) HOL Light and ProofPower-HOL both share all the strengths listed by Ramana with the possible exception of documentation in the case of HOL Light and of libraries (for things like hardware verification) in the case of ProofPower-HOL. Regards, Rob. > On 3 May 2016, at 08:54, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote: > > Some strengths of HOL4 (off the top of my head, so maybe not comprehensive): > • It is based on simple type theory. See "The seven virtues of simple > type theory". > • It is implemented in Standard ML. This is a formally specified > programming language with multiple implementations. > • It exposes APIs that make it relatively easy to write theorem-proving > automation. It is highly programmable. > • It can export proofs in a standard format (OpenTheory). It also has > an implementation-independent representation of saved theories. > • It is a suite of tools following the Unix philosophy. > • It has reasonably large libraries and various big and interesting > examples, including CakeML. > • It is being actively improved and developed, and is free software. > • It has reasonably thorough documentation (not perfect, but pretty > good). > > On 3 May 2016 at 17:34, Ada <956066...@qq.com> wrote: > Hi,guys > I am working with HOL4. Recently, I read some papers, knowing that there > are some other theorem provers, like PVS,COQ. They are similar in many > aspects. For > example, the logic used by them is Higher order logic. I am wondering What is > the advantage of HOL4? > Thanks! > > ------------------------------------------------------------------------------ > Find and fix application performance issues faster with Applications Manager > Applications Manager provides deep performance insights into multiple tiers of > your business applications. It resolves application problems quickly and > reduces your MTTR. Get your free trial! > https://ad.doubleclick.net/ddm/clk/302982198;130105516;z > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------------------------ > Find and fix application performance issues faster with Applications Manager > Applications Manager provides deep performance insights into multiple tiers of > your business applications. It resolves application problems quickly and > reduces your MTTR. Get your free trial! > https://ad.doubleclick.net/ddm/clk/302982198;130105516;z_______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Find and fix application performance issues faster with Applications Manager Applications Manager provides deep performance insights into multiple tiers of your business applications. It resolves application problems quickly and reduces your MTTR. Get your free trial! https://ad.doubleclick.net/ddm/clk/302982198;130105516;z _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
