English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

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: 2005-08-09 (11:34)
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/vectors.ml";;

   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)