• # HOL

• Referenced in 417 articles [sw05492]
• Higher Order Logic (HOL) is a programming environment in which theorems can be proved ... programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform...
• # HOL Light

• Referenced in 253 articles [sw06580]
• HOL Light: an overview. HOL Light is an interactive proof assistant for classical higher-order ... simplified version of Mike Gordon’s original HOL system. Theorem provers in this family ... both the implementation and interaction language; in HOL Light’s case this is Objective CAML ... retaining this reliability and programmability from earlier HOL systems, HOL Light is distinguished...
• # LCF

• Referenced in 148 articles [sw08360]
• mechanized logic of computation. From LCF to HOL: a short history. The original LCF system ... descendents of LCF is HOL, a proof assistant for higher order logic originally developed ... Robin Milner to the development of HOL is remarkable. Not only did he invent ... both by ML and the LCF and HOL logics. Code Milner wrote is still...
• # Flyspeck

• Referenced in 96 articles [sw10277]
• show the Flyspeck formal development (in HOL Light) and the Flyspeck informal mathematical text ... generic and easily adapted to the HOL Light case...
• # CVC Lite

• Referenced in 51 articles [sw07581]
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite This paper ... provers. We define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite ... translates the resulting proof object back to HOL-Light. As a result, we obtain ... while also fundamentally expanding the capabilities of HOL-Light...
• # ProofPower

• Referenced in 41 articles [sw06339]
• implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. ProofPower provides ... using a semantic embedding of Z into HOL. The DAZ tool supporting refinement...
• # HOLyHammer

• Referenced in 18 articles [sw11553]
• HOL(y)Hammer: online ATP service for HOL Light. HOL(y)Hammer is an online ... formal (computer-understandable) mathematics encoded in the HOL Light system. The service allows its users ... arbitrary formal development (project) based on HOL Light, and to attack arbitrary conjectures that...
• # PRocH

• Referenced in 11 articles [sw10191]
• PRocH: Proof Reconstruction for HOL Light. PRocH is a proof reconstruction tool that imports ... HOL Light proofs produced by ATPs on the recently developed translation of HOL Light ... obtained by re-playing in the HOL logic the detailed inference steps recorded ... TPTP) proofs, using several internal HOL Light inference methods. These methods range from fast variable...
• # HOL Zero

• Referenced in 10 articles [sw17594]
• HOL zero’s solutions for Pollack-inconsistency. HOL Zero is a basic theorem prover that ... manages to avoid problems suffered in other HOL systems related to the parsing and pretty ... printing of HOL types, terms and theorems, with the goal of achieving well-behaved parsing/printing...
• # HOL-Z

• Referenced in 11 articles [sw02996]
• HOL-Z is a proof environment for Z built as plug-in of the generic ... checked by the Java-based ZeTa-System. HOL-Z then allows for the formal analysis...
• # HOL-Omega

• Referenced in 8 articles [sw06581]
• HOL-Omega logic A new logic is posited for the widely used HOL theorem prover ... universal types. The new system, called HOL-Omega or $mathrm{HOL} _{omega }$, is a merging...
• # HOL-TestGen

• Referenced in 9 articles [sw17720]
• HOL-TestGen is a is a test case generator for specification based unit testing ... HOL-TestGen is built on top of the specfication and theorem proving environment Isabelle/HOL...