
HOL
 Referenced in 482 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 286 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 ... 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 157 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 107 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 138 articles
[sw04599]
 semiautomated reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success in actually...

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

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 56 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 20 articles
[sw11553]
 HOL(y)Hammer: online ATP service for HOL Light. HOL(y)Hammer is an online ... formal (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...

HOLOCL
 Referenced in 21 articles
[sw05734]
 HOLOCL : Experiences, consequences and design choices Based on experiences gained from an embedding...

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

Isabelle/jEdit
 Referenced in 26 articles
[sw06432]
 HOL [5, {S}1]) with sophisticated frontend technology on the JVM platform, overcoming command...

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

HOL Zero
 Referenced in 12 articles
[sw17594]
 HOL zero’s solutions for Pollackinconsistency. 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 wellbehaved parsing/printing...

MaSh
 Referenced in 21 articles
[sw08206]
 research in the context of Mizar and HOL Light, with a number of enhancements. MaSh...

HOLBoogie
 Referenced in 14 articles
[sw00409]
 paper, however, we present a proofenvironment, HOLBoogieP, 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 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...

HOLZ
 Referenced in 11 articles
[sw02996]
 HOLZ is a proof environment for Z built as plugin of the generic ... checked by the Javabased ZeTaSystem. HOLZ then allows for the formal analysis...

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

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