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 1A04D7F706 for ; Wed, 15 Jan 2014 18:00:30 +0100 (CET) Received-SPF: Neutral (mail2-smtp-roc.national.inria.fr: domain of simon.cruanes.2007@m4x.org does not assert whether or not 129.104.30.34 is permitted sender) identity=pra; client-ip=129.104.30.34; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="SRS0=YdpC=WV=m4x.org=simon.cruanes.2007@bounces.m4x.org"; x-sender="simon.cruanes.2007@m4x.org"; x-conformance=sidf_compatible; x-record-type="spf2.0" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of SRS0=YdpC=WV=m4x.org=simon.cruanes.2007@bounces.m4x.org designates 129.104.30.34 as permitted sender) identity=mailfrom; client-ip=129.104.30.34; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="SRS0=YdpC=WV=m4x.org=simon.cruanes.2007@bounces.m4x.org"; x-sender="SRS0=YdpC=WV=m4x.org=simon.cruanes.2007@bounces.m4x.org"; x-conformance=sidf_compatible; x-record-type="spf2.0" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@mx1.polytechnique.org designates 129.104.30.34 as permitted sender) identity=helo; client-ip=129.104.30.34; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="SRS0=YdpC=WV=m4x.org=simon.cruanes.2007@bounces.m4x.org"; x-sender="postmaster@mx1.polytechnique.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgQCANC91lKBaB4inGdsb2JhbABZFoMtvG0WDgEBAQEBCBQJPINhNAVJiBcNmRKrEZIqgRMElDqDZYExlBM X-IPAS-Result: AgQCANC91lKBaB4inGdsb2JhbABZFoMtvG0WDgEBAQEBCBQJPINhNAVJiBcNmRKrEZIqgRMElDqDZYExlBM X-IronPort-AV: E=Sophos;i="4.95,664,1384297200"; d="scan'208";a="53402271" Received: from mx1.polytechnique.org ([129.104.30.34]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 15 Jan 2014 18:00:29 +0100 Received: from emmental.inria.fr (emmental.inria.fr [128.93.0.14]) (using TLSv1 with cipher ECDHE-RSA-AES128-SHA (128/128 bits)) (No client certificate requested) by ssl.polytechnique.org (Postfix) with ESMTPSA id 266B7140E1820 for ; Wed, 15 Jan 2014 18:00:29 +0100 (CET) Date: Wed, 15 Jan 2014 18:00:28 +0100 From: Simon Cruanes To: OCaml users Message-ID: <20140115170027.GA11251@emmental.inria.fr> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="M9YpAf2t6OxtMGzg" Content-Disposition: inline User-Agent: Mutt/1.5.21 (2010-09-15) X-AV-Checked: ClamAV using ClamSMTP at svoboda.polytechnique.org (Wed Jan 15 18:00:29 2014 +0100 (CET)) X-Spam-Flag: No, tests=bogofilter, spamicity=0.000682, queueID=4CBD8140E1822 X-Org-Mail: simon.cruanes.2007@polytechnique.org Subject: [Caml-list] [ANN] release of Logtk 0.2 --M9YpAf2t6OxtMGzg Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Hello, I'm happy to announce the release of Logtk 0.2, a pure OCaml library for (mostly) first-order logic. It focuses on data structures to represent terms, formulas, types, and provides various algorithms. It is released under the BSD license. - main page: https://www.rocq.inria.fr/deducteam/Logtk/index.html - github: https://github.com/c-cube/logtk - api doc: http://cedeela.fr/~simon/software/logtk/ The library is currently in a working (*) but unstable state, the API may change. I'd be very happy to have feedback about bugs, or about the general usability of the code. Some algorithms and data structures (extract from README): - terms - formulas - types (simple polymorphism) - substitutions (for free variables, bound variables use De Bruijn indices) - first-order unification and matching - simplification term ordering (RPO, KBO) - indexing structures for unification/matching (discrimination trees...) - term rewriting - congruence closure - reduction of formulas to CNF (clausal normal form) - parser for TPTP To give more context, I use this library for small-ish tools that process TPTP files, and for an experimental theorem prover for first-order logic. Yes, it's PhD code ;) Regards, --=20 Simon (*) bugs excepted... --M9YpAf2t6OxtMGzg Content-Type: application/pgp-signature -----BEGIN PGP SIGNATURE----- Version: GnuPG v1 iQIcBAEBAgAGBQJS1r6rAAoJEErAHQhJqmK2Ia8QAM/DDJmE/W1GBKxIl5cTO59t oSAsL07C9PFSDzuQIr6DffEAXOUhQXzSMK5AyHCAzp1PQW50ukSafoupgQT9OSUg gsL0V+fj6Q4rCe3k1RVBL18TXRbcrt2rqKNQYc8A2pAf0CMnZ7P2+7XFvJnodUke O1pD232s87/5cZdMyEDm1v3nLkQmclcK5B50PybrsRtCeOHvJPfmzJ/ARSa73Hm4 iCxzcOBZX0oPhgXvLX1/L7wlUmGmE6ab0h/8o3XCuznG9zQvLLxYt1NygdopjU79 VZbIdGvH4hjNOSQEjGUWawpEHzxiPfr25OsVtuB0Zr3gvYjnDNzRugpHuO+17UN9 R9E43WMPEU5ueOQISlvUsqB4SA5KetBItbO7l+hUT33EmAO6JMRrSVwMRWvZn19J CyfiAJUjlwKFJsw4uTOQZk3XDLZuFHXw32Yp9eax+dj7dR/wlUDuQAwn6+sMrx5m ZpoDp2vFynlVkUTR+aZvwizfclnqEmgMt+L86icNxiQO67SqD5mxp1d5A4QeI15R O3WzQqyQCIhTIci8jgLYVeso1tv/+ivCc+1Xog2A9ByNsdFtuWghIoHYOMhg+awv PN5uz3PI16MJpbLVqxQl/PJtBxU6D/b+2DAe4uLaYxqjZsIm6hKMEMAv9d4JhuOC YPsNT4zZImT473lWC4RE =z0mT -----END PGP SIGNATURE----- --M9YpAf2t6OxtMGzg--