• HOL

  • Referenced in 436 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 257 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 149 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 98 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...
  • Isar

  • Referenced in 125 articles [sw04599]
  • semi-automated reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success in actually...
  • 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...
  • Jordan

  • Referenced in 63 articles [sw23624]
  • Jordan curve theorem (60,000 lines of HOL Light proof scripts, distributed as a library ... HOL Light system...
  • ProofPower

  • Referenced in 49 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...
  • HOL-OCL

  • Referenced in 21 articles [sw05734]
  • HOL-OCL : Experiences, consequences and design choices Based on experiences gained from an embedding...
  • Ott

  • Referenced in 25 articles [sw00663]
  • them into proof assistant code for Coq, HOL, and Isabelle/HOL, together with LaTeX code...
  • HOL/SPIN

  • Referenced in 24 articles [sw02987]
  • HOL/SPIN We provide a proof using HOL and SPIN of convergence for the Routing Information...
  • Isabelle/jEdit

  • Referenced in 22 articles [sw06432]
  • HOL [5, {S}1]) with sophisticated front-end technology on the JVM platform, overcoming command...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • paper, however, we present a proof-environment, HOL-BoogieP, that combines Boogie with the interactive...
  • 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...
  • MaSh

  • Referenced in 17 articles [sw08206]
  • research in the context of Mizar and HOL Light, with a number of enhancements. MaSh...
  • 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...