
HOL Light
 Referenced in 295 articles
[sw06580]
 HOL Light: an overview. HOL Light is an interactive proof assistant for classical higherorder ... 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 HOLLight and CVC Lite This paper ... define a derived rule in HOLLight, CVC_PROVE, which calls CVC Lite and translates ... resulting proof object back to HOLLight. As a result, we obtain a highly trusted ... also fundamentally expanding the capabilities of HOLLight...

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 ... computerunderstandable) 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 replaying 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 HOLLight. Type inference is semiautomatic, 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 hollight 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...