New OCaml version of HOL Light theorem prover
 John Harrison
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ 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/hollight HOL Light proves theorems in classical higherorder 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 preproved 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 "nonobvious" theorem of predicate calculus, using pure firstorder 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.