From: Simon Cruanes <simon.cruanes.2007@m4x.org>
To: OCaml users <caml-list@inria.fr>
Subject: [Caml-list] [ANN] release of Logtk 0.2
Date: Wed, 15 Jan 2014 18:00:28 +0100 [thread overview]
Message-ID: <20140115170027.GA11251@emmental.inria.fr> (raw)
[-- Attachment #1: Type: text/plain, Size: 1283 bytes --]
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,
--
Simon
(*) bugs excepted...
[-- Attachment #2: Type: application/pgp-signature, Size: 819 bytes --]
reply other threads:[~2014-01-15 17:00 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=20140115170027.GA11251@emmental.inria.fr \
--to=simon.cruanes.2007@m4x.org \
--cc=caml-list@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