Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
New OCaml version of HOL Light theorem prover
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: John Harrison <John.Harrison@c...>
Subject: New OCaml version of HOL Light theorem prover

I'm pleased to announce the availability of the HOL Light theorem prover
version 2.0, based on Objective Caml. The system and its documentation,
including a new draft tutorial, can be downloaded from the following Web

HOL Light proves theorems in classical higher-order logic. It is intended
as an interactive proof assistant, but offers automated support for
proofs in some domains (arithmetic, algebra, pure logic...) and has a
significant library of pre-proved mathematics, particularly elementary
analysis. The system is designed to be fully programmable; not only is
OCaml the implementation language but the OCaml toplevel is the "shell"
from which the user directs proofs. Here are the proofs of a few
extremely simple theorems in the system, just to show you what it looks

1. The sum of squares of the first n natural numbers, by induction and

   let SUM_OF_SQUARES = prove
    (`!n:num. nsum(1..n) (\i. i * i) = (n * (n + 1) * (2 * n + 1)) DIV 6`,

2. Vector version of Pythagoras's theorem, using algebra on vectors and real

   needs "Multivariate/";;

   let PYTHAGORAS = prove
    (`!A B C:real^2.
           orthogonal (A - B) (C - B)
           ==> dist(A,C) pow 2 = dist(B,A) pow 2 + dist(B,C) pow 2`,
     SIMP_TAC[dist; NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN

3. Los's "non-obvious" theorem of predicate calculus, using pure
   first-order reasoning.

   let LOS = prove
    (`(!x y z. P x y /\ P y z ==> P x z) /\
      (!x y z. Q x y /\ Q y z ==> Q x z) /\
      (!x y. P x y ==> P y x) /\
      (!x y. P x y \/ Q x y)
      ==> (!x y. P x y) \/ (!x y. Q x y)`,

The ASCIIfied logical symbols used above include:

 !x.    for all x
 /\     and
 \/     or
 ==>    implies
 \x.    lambda x (like "fun x ->" in OCaml)