
HOL
 Referenced in 379 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 243 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 141 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...

Isar
 Referenced in 123 articles
[sw04599]
 semiautomated 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 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 40 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 (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 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...

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...

HOL Zero
 Referenced in 10 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...

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...

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

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

HOLOmega
 Referenced in 8 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...

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