From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id EF2937F02D; Tue, 21 Oct 2014 11:58:56 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of francois.pessaux@ensta-paristech.fr) identity=pra; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="francois.pessaux@ensta-paristech.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of francois.pessaux@ensta-paristech.fr designates 147.250.10.4 as permitted sender) identity=mailfrom; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="francois.pessaux@ensta-paristech.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@ns4.ensta.fr designates 147.250.10.4 as permitted sender) identity=helo; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="postmaster@ns4.ensta.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoUBAMQjRlST+goEmWdsb2JhbABcg2FYgwa5M41xgWyIYhYBEQEBAQEBCAsLBxQuhCx1AT0CXwGIUa5mlHsBAQEek082gR4Fj2WDI4M/gkSGO4V8kjNqgksBAQE X-IPAS-Result: AoUBAMQjRlST+goEmWdsb2JhbABcg2FYgwa5M41xgWyIYhYBEQEBAQEBCAsLBxQuhCx1AT0CXwGIUa5mlHsBAQEek082gR4Fj2WDI4M/gkSGO4V8kjNqgksBAQE X-IronPort-AV: E=Sophos;i="5.04,761,1406584800"; d="scan'208,217";a="102189034" Received: from ns4.ensta.fr ([147.250.10.4]) by mail2-smtp-roc.national.inria.fr with ESMTP; 21 Oct 2014 11:58:56 +0200 Received: from ns4.ensta.fr (localhost [127.0.0.1]) by ns4.ensta.fr (Postfix) with ESMTP id 85AE8CAB0D; Tue, 21 Oct 2014 11:58:56 +0200 (CEST) X-Virus-Scanned: amavisd-new at ns4.ensta.fr Received: from ns4.ensta.fr ([127.0.0.1]) by ns4.ensta.fr (ns4.ensta.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id qNcnl_iwf5Gq; Tue, 21 Oct 2014 11:58:56 +0200 (CEST) Received: from zemail.ensta.fr (zemail.ensta.fr [147.250.1.16]) by ns4.ensta.fr (Postfix) with ESMTP id 14F57CAB0A; Tue, 21 Oct 2014 11:58:56 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 0BF9929714C; Tue, 21 Oct 2014 11:58:56 +0200 (CEST) Received: from zemail.ensta.fr ([127.0.0.1]) by localhost (zemail.ensta.fr [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id cWeocFU0d6_i; Tue, 21 Oct 2014 11:58:55 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 90CD3297151; Tue, 21 Oct 2014 11:58:55 +0200 (CEST) X-Virus-Scanned: amavisd-new at zemail.ensta.fr Received: from zemail.ensta.fr ([127.0.0.1]) by localhost (zemail.ensta.fr [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id de_utVuuVaE9; Tue, 21 Oct 2014 11:58:55 +0200 (CEST) Received: from [147.250.222.31] (unknown [147.250.222.31]) by zemail.ensta.fr (Postfix) with ESMTPSA id 74C6029714C; Tue, 21 Oct 2014 11:58:55 +0200 (CEST) From: =?utf-8?Q?Fran=C3=A7ois_Pessaux?= Content-Type: multipart/alternative; boundary="Apple-Mail=_DAF83D4F-C18D-4B6C-B102-A473BB818003" Message-Id: <63A6A559-2805-4645-81CC-5FECBB396F92@ensta-paristech.fr> Date: Tue, 21 Oct 2014 11:58:55 +0200 To: caml-list@inria.fr, focalize-devel FoCaLize-Devel , focalize-users FoCaLiZe-Users Mime-Version: 1.0 (Mac OS X Mail 8.0 \(1990.1\)) X-Mailer: Apple Mail (2.1990.1) Subject: [Caml-list] [Announce] Release 0.8.0 of Zenon --Apple-Mail=_DAF83D4F-C18D-4B6C-B102-A473BB818003 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Greetings, It is my pleasure to announce (for Damien Doligez ^_^) the release of Zenon, an automatic theorem prover written in OCaml. Zenon handles first-order logic with equality. Its most important feature = is that it outputs the proofs of the theorems, in Coq-checkable form. This is version 0.8.0, available at < http://sosie.inria.fr > (and soon at < http://zenon-prover.org >) with several is= sues fixed since the last release. Unfortunately, there is no documentation yet, so this is for the adventurous spirit. It is released under the New BSD license. =E2=80=94 Fran=C3=A7ois for Damien --Apple-Mail=_DAF83D4F-C18D-4B6C-B102-A473BB818003 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
Gr= eetings,
It is my pleasure to announce (for Damien Dol= igez ^_^) the release of Zenon,
an automatic theorem p= rover written in OCaml.

Zenon handles first-order logic with equality.  Its most import= ant feature is
that it outputs the proofs of the theor= ems, in Coq-checkable form.

This is version 0.8.0, available at < http://sosie.inria.fr > (and soon
at  < http://zenon-prover.org >) with several issues f= ixed since the
last release.

Unfortunately, there is no documentation y= et, so this is for the
adventurous spirit.

It is released under the New= BSD license.

 =E2=80=94 Fran=C3=A7ois fo= r Damien

= --Apple-Mail=_DAF83D4F-C18D-4B6C-B102-A473BB818003--