From: John Harrison <John.Harrison@cl.cam.ac.uk>
To: caml-list@yquem.inria.fr
Cc: John.Harrison@cl.cam.ac.uk
Subject: New OCaml version of HOL Light theorem prover
Date: Tue, 09 Aug 2005 12:34:04 +0100 [thread overview]
Message-ID: <E1E2SMu-0006UW-00@mta1.cl.cam.ac.uk> (raw)
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.
reply other threads:[~2005-08-09 11:34 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=E1E2SMu-0006UW-00@mta1.cl.cam.ac.uk \
--to=john.harrison@cl.cam.ac.uk \
--cc=caml-list@yquem.inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).