• HOL Light

  • Referenced in 295 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 ... implementation and interaction language; in HOL Light’s case this is Objective CAML (OCaml). Thanks ... programmability from earlier HOL systems, HOL Light is distinguished by its clean and simple design...
  • Flyspeck

  • Referenced in 113 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 55 articles [sw07581]
  • theorem provers: a case study combining HOL-Light and CVC Lite This paper ... define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite and translates ... resulting proof object back to HOL-Light. As a result, we obtain a highly trusted ... also fundamentally expanding the capabilities of HOL-Light...
  • Jordan

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

  • Referenced in 21 articles [sw11553]
  • Hammer: online ATP service for HOL Light. HOL(y)Hammer is an online AI/ATP service ... 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...
  • MaSh

  • Referenced in 22 articles [sw08206]
  • context of Mizar and HOL Light, with a number of enhancements. MaSh outperforms...
  • PRocH

  • Referenced in 12 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...
  • miz3

  • Referenced in 11 articles [sw18631]
  • called miz3 , on top of the HOL Light interactive theorem prover. The declarative language that ... tactics and formal libraries of HOL Light, and as such has ‘industrial strength’. Our approach...
  • OpenTheory

  • Referenced in 15 articles [sw32625]
  • implementations of higher order logic, including HOL Light, HOL4 and ProofPower. It is hoped that...
  • HOL Light QE

  • Referenced in 3 articles [sw28656]
  • HOL Light QE. We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ... quotation and evaluation to HOL Light to demonstrate the implementability of CTTqe and the benefits ... assistant. The resulting system is called HOL Light QE. Here we document the design ... HOL Light QE and the challenges that needed to be overcome. The resulting implementation...
  • HOL2P

  • Referenced in 4 articles [sw21180]
  • been implemented on top of HOL-Light. Type inference is semi-automatic, and some type...
  • Tactician

  • Referenced in 3 articles [sw17591]
  • helping you maintain and/or understand HOL Light proof scripts. Its main function is to refactor...
  • Quaternions

  • Referenced in 1 article [sw38038]
  • This theory is inspired by the HOL Light development of quaternions, but follows ... must be proved explicitly in the HOL Light version. The development concludes with the geometric...
  • HipCam

  • Referenced in 1 article [sw17592]
  • HipCam: Tools for recording Hiproofs in hol-light and visualising them in a web browser...
  • WorkflowFM

  • Referenced in 1 article [sw21519]
  • processes paradigm within the proof assistant HOL Light. This enables the specification of abstract processes...
  • ACL2

  • Referenced in 279 articles [sw00060]
  • ACL2 is both a programming language in which...
  • BIGEBRA

  • Referenced in 19 articles [sw00078]
  • Clifford and Graßmann Hopf algebras via the BIGEBRA...
  • CLIFFORD

  • Referenced in 80 articles [sw00131]
  • CLIFFORD performs various computations in Grass mann and...
  • CLUCalc

  • Referenced in 33 articles [sw00133]
  • CLUCalc is a freely available software tool for...
  • Coq

  • Referenced in 1818 articles [sw00161]
  • Coq is a formal proof management system. It...