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
• John Harrison
[ 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 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.

```