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...