Version française
Home     About     Download     Resources     Contact us    
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
page:

  http://www.cl.cam.ac.uk/users/jrh/hol-light

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

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

   let SUM_OF_SQUARES = prove
    (`!n:num. nsum(1..n) (\i. i * i) = (n * (n + 1) * (2 * n + 1)) DIV 6`,
     INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;

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

   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
     CONV_TAC REAL_RING);;

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)`,
     MESON_TAC[]);;

The ASCIIfied logical symbols used above include:

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

John.